[M3devel] LockHeap

[mika at async.caltech.edu]

The code in LockHeap looks dubious to me:

VAR
  holder: pthread_t;
  inCritical := 0;

PROCEDURE LockHeap () =
  VAR self := pthread_self();
  BEGIN
    WITH r = pthread_mutex_lock(heapMu) DO <*ASSERT r=0*> END;
    IF inCritical = 0 THEN
      holder := self;
    ELSIF pthread_equal(holder, self) = 0 THEN
      WITH r = pthread_cond_wait(heapCond, heapMu) DO <*ASSERT r=0*> END;
    END;
    INC(inCritical);
    WITH r = pthread_mutex_unlock(heapMu) DO <*ASSERT r=0*> END;
  END LockHeap;

My understanding is that this code is relatively simple in that there's
a single pthread mutex, heapMu, that protects holder and inCritical.

All it's trying to do is build a "reentrant" mutex (of the kind Dragisa
was asking for a while back).  To annotate a bit:

PROCEDURE LockHeap () =
  VAR self := pthread_self();
  BEGIN
    WITH r = pthread_mutex_lock(heapMu) DO <*ASSERT r=0*> END;
    
    (* heapMu locked --- only a single thread can be here *)

    IF inCritical = 0 THEN
      holder := self;
    ELSIF pthread_equal(holder, self) = 0 THEN
      WITH r = pthread_cond_wait(heapCond, heapMu) DO <*ASSERT r=0*> END;
      (* heapMu locked *)
    END;
    INC(inCritical);


    WITH r = pthread_mutex_unlock(heapMu) DO <*ASSERT r=0*> END;

    (* heapMu unlocked *)

  END LockHeap;

Based on the assertions in UnlockHeap it seems that the postcondition of LockHeap
should be { holder = self AND inCritical > 0 }.

So we check if inCritical is 0 -- no one else wants the critical section.  OK: mark
self as holder and return.

Next we check if we already have the critical section (pthread_equal() # 0).  If we do,
ok, just return, we're done.

If neither of those succeeds, we wait for ... what, actually?
If neither succeeds, that means another thread is in the critical
section.  We need to wait for it to release the critical section.
Doesn't that mean that we have to wait for the condition { inCritical =
0 OR pthread_equal(holder,self) # 0 }?  Since we're a single thread here,
we actually need only wait for inCritical = 0....

In any case, my coding of this would be:

PROCEDURE LockHeap () =
  VAR self := pthread_self();
  BEGIN
    WITH r = pthread_mutex_lock(heapMu,ThisLine()) DO <*ASSERT r=0*> END;
    LOOP
      IF inCritical = 0 THEN
        holder := self; 
        EXIT
      ELSIF pthread_equal(holder,self) # 0 THEN
        EXIT
      ELSE
        WITH r = pthread_cond_wait(heapCond, heapMu, ThisLine()) DO <*ASSERT r=0*> END;
      END     
    END;
    INC(inCritical);
    <*ASSERT pthread_equal(holder, self) # 0*>
    WITH r = pthread_mutex_unlock(heapMu,ThisLine()) DO <*ASSERT r=0*> END;
  END LockHeap;


(it makes more logical sense to have the pthread_equal test first, but it is probably much
faster to check inCritical so let's check that first).

I'm not sure how this could have gotten screwed up?  It seems really basic.. unless I'm
misunderstanding the code.

I note that the documentation in RTOS.i3 also seems slightly incorrect:

PROCEDURE WaitHeap (VAR thread: RTHeapRep.ThreadState);

     Blocks the caller until BroadcastHeap has been called and the allocator/collector critical section is released. The caller must be in the critical section.

Shouldn't it say "The calling thread must have entered the critical
section exactly once."?  (Given that the "LockHeap" is reentrant...)

Why is there a reentrant mutex here, anyhow?

     Mika