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

Question

我想要一个 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 模型有效地测试它

到目前为止，我有一个简单的模型，如下使用它：

（完整示例--> 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

免责声明：虽然我的博士学位是形式化方法，但我已经 15 年没有做过任何模型了，而且我从未使用过 Promela。

这是我的笔记。

1. acquire_write

   应等待所有读者释放锁。您检查

   lock.writing == 0

   ，但是

   lock.readers > 0

   呢？

尝试以下场景：

Reader does acquire_read and proceeds
Writer does acquire_write and ?

据我们所见，

Writer

继续进行，而规范要求它阻止。

2. 我相信，

   acquire_read

   没有满足以下要求：

如果任何 Goroutine 在锁已被一个或多个读取者持有时调用 Lock，则对 RLock 的并发调用将阻塞，直到写入者获取（并释放）该锁，以确保该锁最终可供写入者使用。

模型

acquire_read

不仅应该在

lock.writing == 1

时等待，而且还应该在

lock.writeWaiters > 0

时等待。

尝试以下场景：

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

根据规范，它应该被阻止。根据你的模型，它会继续

lock.readers++

，不是吗？

3. 订购。

规范要求：

对于任何对 RLock 的调用，都存在一个 n，使得对 Unlock 的第 n 次调用“在对 RLock 的调用之前同步”，并且对 RUnlock 的相应调用在对 Lock 的第 n+1 次调用“之前同步”。

我找不到模型如何形式化它。

尝试以下场景：

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 
*/