« earlier | later » Page 1 of 1
Axiomatic validation of memory barriers and atomic instructions [LWN.net] edit / delete
More progress on model checking for memory models on modern processors. The tool described here covers ARM, Power and x86 memory models, and does efficient analysis of (smallish) chunks of code.
to arm atomic concurrency herd intel memory memory-model model-checking power static-analysis x86 ... on 28 August 2014
IPC Protocols - MozillaWiki edit / delete
Protocol specifications from the Mozilla project (they plan to model-check using SPIN).
to concurrency ipc model-checking mozilla spin ... on 03 April 2012
Model-checker for Erlang, using a modified runtime library (much like Neil's CHP-to-CSP trick).
to concurrency erlang model-checking ... on 01 June 2009
« earlier | later » Page 1 of 1
| - model-checking | |
| 1 | + arm |
| 1 | + atomic |
| 3 | + concurrency |
| 1 | + erlang |
| 1 | + herd |
| 1 | + intel |
| 1 | + ipc |
| 1 | + memory |
| 1 | + memory-model |
| 1 | + mozilla |
| 1 | + power |
| 1 | + spin |
| 1 | + static-analysis |
| 1 | + x86 |
tasty by Adam Sampson.