[Maude-users] On threading

[Steven Eker]

It's straightforward to specify a deep embedding of a parallel imperative 
language in Maude; see 

Steven Eker, José Meseguer and Ambarish Sridharanarayanan. 
The Maude LTL Model Checker. 
In 4th International Workshop on Rewriting Logic and its Applications 
(WRLA'02). 

although a language as intricate as C++ would be quite tedious. You could then 
check LTL properties of programs written in the parallel imperative language 
with the Maude model checker (assuming only a finite number of states are 
reachable); though it may be slower than SPIN because it lacks partial order 
reduction and some other optimization that are hard in such a general setting 
as rewriting logic.

How did you get your C++ code into SPIN? do you have a verified translator?

Steven

On Tuesday 31 January 2006 13:55, gshanemiller at comcast.net wrote:
> All,
>
> I recently completed an analysis on some pthreads based C++ code using
> AT&T's SPIN. The code purported to implement a concurrent event queue in
> which a producer thread(s) would add events to a queue whilst consumer
> thread(s) removed events from that queue. It used a pthread condition
> instance to eliminate  a busy-wait-loop.
>
> SPIN did a very good job at answering fundamental questions to include:
>
> * did the code deadlock? (it did not)
> * could any of the threads be starved for CPU cycles? (nope)
> * were all states reachable? (no, some were not reachable.)
> * did the producer thread(s) signal consumers only when data was there?
>    (no it did not; bug)
> * did the consumer thread(s) try to remove events only when data was
>    in the queue? (no, there was a bug for two or more get threads)
> * process of modeling code helped identify numerous other technical
>    glitches and inefficiences.
>
> All in all, a very good exercise.
>
> How would one approach answering these same questions in Maude?
>
> Shane Miller
> _______________________________________________
> Maude-users mailing list
> Maude-users at maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-users