fmjs/emme

EMME: ECMAScript Memory Model Evaluator

EMME: ECMAScript Memory Model Evaluator

This tools provides a SAT/SMT-based verification for JavaScript programs with shared array memory access (i.e., SharedArrayBuffer).

Learn more.

Briefly, given a JavaScript-like SharedArrayBuffer bounded execution program (see .bex files in the examples folder), EMME computes all valid executions according with the ECMA specification (http://tc39.github.io/ecmascript_sharedmem/shmem.html). The valid executions are provided as: 1) a set of graphviz files represeting the memory model relations (i.e., mm*.dot), and 2) an assertion on the automatically generated JavaScript program (i.e., program.js).

Installation

Using Docker:

1. install Docker with your package manager e.g., sudo apt-get install docker
2. build the Docker image: cd docker/fedora_64 && docker build -f fedora-emme .
3. run the Docker image: docker run -i -t fedora-emme /bin/bash

On Linux and MacOS:

1. install python package dependencies: pip install -r requirements.txt
2. install CVC4 SMT solver (see http://cvc4.cs.stanford.edu/ for licensing and additional informations): cd ext_tools && bash get_CVC4.sh && cd ..
3. install V8 JS engine (see https://developers.google.com/v8/ for licensing and additional informations): cd ext_tools && bash get_v8.sh && cd ..

Usage

To start playing with the tool, you can run:

1. python emme.py examples/single_var/sv_simple01.bex (to generate the valid executions in the folder examples/single_var/sv_simple01/)
2. python litmus.py -c "bash ext_tools/run_v8.sh" -i examples/single_var/sv_simple01/program.js -n 1k -j 4 (to check if the d8 engine obeys the expected results)
3. python emme.py examples/single_var/sv_simple01.bex --unmatched --jsengine="bash ext_tools/run_v8.sh" -n 1k -j 4 (to perform the behavioral coverage constraint analysis)
4. python emme.py examples/single_var/sv_simple01.bex --synth (to generate all equivalent programs in the folder examples/single_var/sv_simple01/)

For more details on the license, have a look at LICENSE.txt

Publications

• "EMME: a formal tool for ECMAScript Memory Model Evaluation". C. Mattarei, C. Barrett, S. Guo, B. Nelson, and B. Smith. TACAS 2018, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Thessaloniki (Greece).

Build Status

emme's Issues

Some expected executions not observed when en_SINGLE_WRITES disabled

Hi Cristian!

I've found EMME very useful for double-checking expectations I've had about the JS memory model. I currently believe that the JS spec mis-specifies "Init" actions, and I tried to use EMME to confirm that the pathological executions I was expecting were exhibited, but it's not giving the output I was expecting.

For the following test, with en_SINGLE_WRITES disabled, I expected to observe 4 valid executions, for each bytewise combination of thread 2 reading from the init event/thread 1's write.
test.zip (see test.bex in the zip)

However, EMME only reported 2 executions, where thread 2 reads from one or the other, but never a bytewise combination. Graphs are included in the above zip.

However, if I add an unrelated read event on a different thread, at a disjoint section of the arraybuffer, I get the 4 executions I was expecting.
test_unrelated_read.zip (see test.bex in the zip)

This seems to be affected by the tear-free reads predicate. In the first example, if I comment this predicate out of the model, I observe the 4 executions I'm expecting. I don't believe that the tear-free reads condition should affect my test, since "Init" events are specified as being one byte in size.