search
Table of Contents
Complex APIs can easily confuse experts with corner cases in short examples. As such, tools to explore these cases and the APIs involved are needed. We are creating a system in which an API is first formalized in first-order logic and then tools are generated to explore the API. The formalization language is called “4M”. A compiler takes takes 4M definitions and outputs a variety of useful data and tools.
Currently the 4M compiler will output a compiled “kernel language” form of the specification for use in “what-if” exploration of scenarios. The C-based Golden Executable model will also use the compiled form with the model to allow running C programs, linked to wrappers, against the API model. There is also an incomplete tool to generate the wrappers from the API specification.
Download
The complete framework for our modeling system of the MCAPI API is located on Github. We also have a separate framework for translating MCAPI executions traces into SMT problems.
Golden Executable Model
The “Golden Executable Model”, or GEM, takes the specification of an API written in 4M and produces a model of the API that can be executed as a drop-in replacement for the C API. It does so by compiling a C program against wrappers that communicate with the API model that runs the compiled “kernel language” form of 4M. This executable model is as correct as the 4M model. (So it depends on the manual translation of a specification from English to 4M.) It has the potential to explore all paths through the API's behavior and avoids potential bugs in a hand-crafted “reference implementation.”
At present the GEM will randomly select one of the several possible next-states to explore, giving a single, randomly chosen path through the program. Future work will include backtracking for an exhaustive exploration of possible behavior.
Formal Specifications
Below are some specifications made using 4M. There are also several small, demo 4M files in the source download above.
MCAPI
The Multicore Association Communication API (MCAPI) is a small message passing library targeting embedded and heterogenous systems. This specification is a subset that deals with the connectionless calls (init, endpoints, send, and receive). It demonstrates handling non-determinism in a concurrent API and non-blocking calls.
Note that the interesting concurrency problems do not exist in the connection-oriented calls, so our efforts have focused on the message-passing calls of MCAPI. We also have not done much with setting or checking endpoint attributes, but the calls are included in the model. Eventually all calls in MCAPI should be included.
MRAPI
The Mutlicore Association Resources API (MRAPI) handles mutexes, locks, conditions, shared memory, and metadata. It is similar to PThreads' handling of the same. This specification does not include metadata.
