[Maude-users] On threading

[Steven Eker]

On Tuesday 31 January 2006 20:22, Shane Miller wrote:
> > Steven Eker, José Meseguer and Ambarish Sridharanarayanan.
> > The Maude LTL Model Checker.
> > In 4th International Workshop on Rewriting Logic and its Applications
> > (WRLA'02).
>
> Does this paper address threading in the way I ask about?

If you regard threading as interleaved processes sharing memory, the Dekker's 
algorithm example has that form. The point about Maude is you can do a deep 
embedding of a language fragment that is just powerful enough to express your 
algorithm. The parallel imperative language in the Dekker's algorithm example 
is defined by 5 rules, one for each program construct (assignment, 
sequencing, if then else fi, while do, repeat). Parallelism is implicit 
because the rules are defined on multisets of processes with a shared memory.
The 5 rules have the same form as the rules you would find in a text on 
programming language semantics, yet because they are written in Maude they 
form an executable specification, and multisets of processes written in the 
language can be executed and model checked. Model checking requires that you 
also define the predicates on state you require using equations.

Steven