how to model golang RWLock using Promela modeling language

Question

I'd like a model of the golang RWMutex API semantics ( https://pkg.go.dev/sync#RWMutex ); in particular I want the blocking behavior for readers and writers.

Here's my model of the read write mutex:

typedef RWLock {
  chan writeComplete = [0] of {bit};
  chan allowWrite = [0] of {bit};
  int readers;
  bit writing;
  int writeWaiters;
  int readWaiters
}


/* RWLock actions */

inline acquire_read(lock) {
  do
    :: atomic {
      if
        :: lock.writing == 1 ->
       lock.readWaiters++;
       lock.writeComplete?0;
       lock.readWaiters--;
       break
        :: else ->
       lock.readers++;
       break
      fi
    }
  od
}

inline release_read(lock) {
    atomic {
      lock.readers--;
      lock.readers == 0 ->
end:   lock.writeComplete!0
    }
}

inline acquire_write(lock) {
  do
    :: atomic {
      if
    :: lock.writing == 0 -> 
       lock.writing = 1;
       break;
    :: else ->
       lock.writeWaiters++;
       lock.allowWrite?0;
       lock.writeWaiters--
      fi
    }
  od
}

inline release_write(lock) {
  atomic {
    assert(lock.writing == 1);
    lock.writing = 0
    if
    :: lock.writeWaiters > 0 ->
        lock.allowWrite!0
    :: else ->
        skip
    fi
    if
    :: lock.readWaiters > 0 ->
        lock.writeComplete!0;
    :: else ->
        skip
    fi
  }
}

I'm not totally sure if this is correct. Ideally answer to my question would be in one of these categories:

1. assure me that my model is correct
2. tell me it's wrong and tell me how to fix it
3. you don't know if it's correct but you can offer some guidance on how I can effectively test this using a promela model

So far I have a naive model that uses it like this:

( complete example here --> https://gist.github.com/david415/05a5e7ed332e90bd7fb78b1f8f0c72cb )

int counter = 0;


proctype Writer(RWLock lock) {
  acquire_write(lock);
  counter = counter + 1;
  printf("Writer incremented counter to %d\n", counter);
end: release_write(lock);
}

proctype Reader(RWLock lock) {
  int localCounter;
  acquire_read(lock);
  localCounter = counter;
  printf("Reader read counter: %d\n", localCounter);
end: release_read(lock);
}

init {
  RWLock myLock;
  myLock.readers = 0;
  myLock.writing = 0;
  myLock.writeWaiters = 0;
  myLock.readWaiters = 0

  run Writer(myLock);
  run Reader(myLock)
end: skip
}

Answer 1

Disclaimer: though my PhD was in Formal Methods, it has been 15 years since I did any models, and I never user Promela.

Here are my notes.

1. acquire_write should wait until all readers release the lock. You check lock.writing == 0, but what about lock.readers > 0?

Try the following scenario:

Reader does acquire_read and proceeds
Writer does acquire_write and ?

As far as can see, Writer proceeds, while the spec requires it to block.

2. I believe, acquire_read doesn't catch the following requirements:

If any goroutine calls Lock while the lock is already held by one or more readers, concurrent calls to RLock will block until the writer has acquired (and released) the lock, to ensure that the lock eventually becomes available to the writer.

The model acquire_read should wait not only when lock.writing == 1, but when lock.writeWaiters > 0 as well.

Try the following scenario:

ReaderA does acquire_read and proceeds
Writer does acquire_write and blocks
ReaderB does acquire_read and ?

According to the spec, it should block. According to your model, it proceeds with lock.readers++, doesn't it?

3. Ordering.

The spec requires:

For any call to RLock, there exists an n such that the n'th call to Unlock “synchronizes before” that call to RLock, and the corresponding call to RUnlock “synchronizes before” the n+1'th call to Lock.

I can't find how the model formalizes it.

Try the following scenario:

ReaderA does acquire_read and proceeds
WriterA does acquire_write and blocks
ReaderB does acquire_read and blocks /* since WriterA.acquire_write is pending */
WriterB does acquire_write and blocks * since WriterB.release_write hasn't been esecuted called yet */
ReaderC does acquire_read and /* blocks since there are pending writers */
ReaderA does release_read
/* Expected (not sure): 
   WriterA unblocks, what about your model?
   WriterB is blocked, 
   ReaderB and ReaderC are blocked due to the ordering requirement: 
     WriterA.acquire_read was before ReaderB.acquire_read 
*/
WriterA does release_write
/* Expected (not sure): 
   ReaderB proceeds, 
   WriterB is blocked due to the ordering requirement: 
     ReaderB.acquire_read was called before WriterB.acquire_read 
   ReaderC is blocked due to pending writer
*/ 
ReaderB does release_read
/* Expected (not sure): 
   WriterB proceedes due to the ordering requirement: 
     it was blocked before ReaderC
   ReaderC 
*/