Differences

This shows you the differences between two versions of the page.

Link to this comparison view

vv-lab:4m [2015/02/18 22:37] (current)
egm created
Line 1: Line 1:
 +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 [https://​github.com/​ericmercer/​4M framework] for our modeling system of the MCAPI API is located on [http://​github.com Github]. We also have a separate framework for translating MCAPI executions traces into [https://​github.com/​ericmercer/​MP-trace-language 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.
 +
 +[[MCAPI|MCAPI formalization work]]
 +
 +=== 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.
vv-lab/4m.txt ยท Last modified: 2015/02/18 22:37 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0