[M3devel] Fwd: Fork bug

[mika at async.caltech.edu]

Hendrik Boom writes:
...
>> While we are working on MUTEX, I would like to propose making them
>> what I believe is meant by a recursive mutex, that is, one thread
>> can lock multiple times, the mutex being released only when the number
>> of unlocks catches up with the number of locks.
>> 
>
>Recursive reentry into a semaphore might just possibly indicate a 
>serious bug in the logic of one's program.  It is not the purpose of 
>Modula 3 to paper over the effects of bad programming, however 
>convenient it seems to be.
>
>Perhaps if you came up with useful, convenient, and elegant proof rules 
>for your desired behaviour, you might convince me otherwise.
>

I agree with these sentiments wholeheartedly.

A link to a paper my graduate advisor wrote years ago:

http://www.async.caltech.edu/~mika/Axiomatic-def.pdf

Modula-3 MUTEX is a restricted form of Dijkstra's P and V operations.
The proof rules in the paper are very simple but not if you allow a
recursive mutex.

    Mika