Overview
We provide a tool, PMCx86, that automatically translates programs written in a subset of the x86 assembly language to Cubicle-W, our extension of the Cubicle model checker that allows to check safety properties of parametrized transition systems under weak memory.
Publications
Compiling Parameterized x86-TSO Concurrent Programs to
Cubicle-W
Sylvain Conchon, David Declerck and Fatiha Zaïdi
In 19th International Conference on Formal Engineering Methods,
Xi'an, China, November 2017
Download
pmcx86 source code and examples
You should also download
Cubicle-W
Compilation
The tool may be compiled using any recent version of the OCaml compiler by typing make in the source folder. It should not require any specific dependency.
Usage
To invoke the tool, simply run the following command:
pmcx86 prog.s
This produces a Cubicle-W file named prog.cub that can then be checked by executing:
cubiclew prog.cub
Experiments
The table below presents the results obtained on some classical x86-TSO programs. For each program, both the x86-TSO and Cubicle-W code is provided. We give some statistics about the program: number of non-weak arrays, number of weak variables and arrays, number of transitions. We then give the length of the counter-example found (if any), and Cubicle-W's running time.
| Program | Non-weak Arrays | Weak Variables |
Weak Arrays | Transitions | Counter-Example Length | Time | |
|---|---|---|---|---|---|---|---|
| Naive Mutex w/ Deadlock x86 Code / Cubicle-W Code | US | 3 | 1 | 1 | 12 | 12 | 0,38s |
| Naive Mutex w/o Deadlock x86 Code / Cubicle-W Code | US | 3 | 1 | 1 | 14 | 12 | 0,85s |
| Mutex w/ xchg x86 Code / Cubicle-W Code | US | 4 | 1 | 0 | 8 | 10 | 0,07s |
| Mutex w/ xchg x86 Code / Cubicle-W Code | S | 3 | 1 | 0 | 7 | - | 0,08s |
| Mutex w/ cmpxchg x86 Code / Cubicle-W Code | US | 4 | 1 | 0 | 10 | 10 | 0,12s |
| Mutex w/ cmpxchg x86 Code / Cubicle-W Code | S | 4 | 1 | 0 | 8 | - | 0,47s |
| Linux Spinlock x86 Code / Cubicle-W Code | US | 4 | 1 | 0 | 10 | 6 | 0,06s |
| Linux Spinlock x86 Code / Cubicle-W Code | S | 4 | 1 | 0 | 9 | - | 0,30s |
| Sense Reversing Barrier (single entry) x86 Code / Cubicle-W Code | S | 3 | 1 | 1 | 15 | - | 0,27s |
| Sense Reversing Barrier (multiple entries) x86 Code / Cubicle-W Code | S | 3 | 1 | 1 | 16 | - | 1m37s |