没有锁和原子的生产者-消费者问题可能吗

Question

我提出了一个似乎适用于单一生产者-单一消费者问题的代码。我没有使用任何锁或原子。我缺什么了吗？

const int LEN = 10;
int q[LEN];
volatile int loc1 = 0;
volatile int loc2 = 0;

void* consumer(void* arg) {
while(1) {
while(loc1 == loc2);
int val = q[loc1];
loc1 = (loc1 + 1) % LEN;
}
pthread_exit(NULL);
}
void* producer(void* arg) {
while(1) {
while((loc2 + 1) % LEN == loc1);
q[loc2] = getItem();
loc2 = (loc2 + 1) % LEN;
}
pthread_exit(NULL);
}

我做了一些压力测试，但没有失败。

生产者中的while循环等待队列中的元素少于LEN-1，然后再生成新元素。我基本上是防止队伍完全排满。

Answer 1

以下是一篇关于没有锁但使用原子的单生产者-单消费者实现的形式证明的文章：https://blog.adacore.com/from-rust-to-spark-formally-proven-bip-buffers