如何使用Promela建模语言对Golang RWLock进行建模

我想要一个golang RWMutex API语义的模型(https://pkg.go.dev/sync#RWMutex);特别是我想要读者和作者的阻塞行为.

下面是我的读写互斥锁模型:

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
  }
}

我不能完全肯定这是不是正确的.理想情况下，我的问题的答案应该是以下几类之一:

1. 向我保证我的模型是正确的
2. 告诉我这是错的，告诉我如何修复它
3. 你不知道它是否正确，但你可以提供一些指导，告诉我如何使用Promela模型有效地测试它

到目前为止，我有一个简单的模型，它是这样使用的:

( complete example here --

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
}