Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On 4/25/13 6:48 AM, smiller wrote:
> Is there a write up that deals with mutual exclusion, race conditions, 
> process, and thread invariants in Maude like what the SPIN MODEL checker 
> excels at?
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
Section 13.6.4 of the Maude book contains a model check of Dekker's 
algorithm. There are more complicated examples in the Maude literature 
if you Google, though some are behind pay walls.

The basic idea when you deal with threads, is to write an interpreter 
(i.e. a deep embedding) for your imperative, threaded language in Maude. 
Depending on the semantics of your language, this can be quite compact. 
You then model check the run of the parallel algorithm you are 
interested in, on that interpreter.

Steven