[M3devel] Fwd: Fork bug

mika at async.caltech.edu mika at async.caltech.edu
Wed Jul 16 08:38:56 CEST 2014

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:


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.


More information about the M3devel mailing list