Let's Prove A Concurrent Blocking Queue (sequel of Let's Prove Leftpad)

栏目: IT技术 · 发布时间: 4年前

内容简介:This is a repository of provably deadlock-free blocking queue.This challenge was inspired byProvably correctis a guarantee that an algorithm satisfies given correctness properties, say deadlock freedom. You do this by providing a

Let's prove a blocking queue deadlock-free

This is a repository of provably deadlock-free blocking queue.

This challenge was inspired by lets-prove-leftpad (from which this README and the contribution guide have been adopted). However, while lets-prove-leftpad is about a sequential algorithm, this challenge is about a concurrent one.

What is "provably-correct"?

Provably correctis a guarantee that an algorithm satisfies given correctness properties, say deadlock freedom. You do this by providing a proof that a computer can check. If the proof is wrong, the computer will tell you that your algorithm is incorrect (wrt correctness properties). Or as Donald Knuth puts it: " Beware of bugs in the above code; I have only proved it correct, not tried it. "

Compare to something like testing: even if you run your test for days and days, you still don't know for sure that keeping it running for another minute won't reveal a deadlock. With a proof, though, you know your algorithm will be deadlock-free after a computer has verified the proof. Proving correctness is really, really powerful. It's also time consuming and often not worth the effort.

This is a sampler of all the different tools we can use to prove algorithms and (implementations) correct, standardized by all being proofs for a simple concurrent data-structure most likely every programmer has encountered in her career.

What is a "blocking queue"?

A queue that blocks until the queue becomes non-empty when consumers retrieve an element, and waits for space to become available when producers store an element. The queue has a fixed/static capacity. For simplicity, we will only consider finite and disjoint sets of producers and consumers. In other words, a producer is blocked if the queue is full; a consumer is blocked if it's empty.

The task is to prove that your blocking queue is guaranteed to never deadlock no matter the queue's capacity, the number of producers, or the number of consumers in the system. If there is space in the queue, some producer will eventually add an element to the queue. If there are elements in the queue, some consumer will eventually remove them from the queue. More formally: Let P and C be the sets of the producer and consumer threads and let W be the set of all waiting/sleeping/blocked threads. Prove that (P \cup C) # W is a valid property of your blocking queue.

Since C is perhaps common ground for most of us, below is a listing of a blocking queue implementation:

#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include <pthread.h>

uint32_t buff_size;
uint32_t *buffer;
uint32_t fillIndex, useIndex, count = 0;

pthread_cond_t empty, full; 
pthread_mutex_t mutex;

void put(uint32_t value) {
	buffer[fillIndex] = value;
	fillIndex = (fillIndex + 1) % buff_size;
	count++;
}

uint32_t get() {
	uint32_t tmp = buffer[useIndex];
	useIndex = (useIndex + 1) % buff_size;
	count--;
	return tmp;
}

void *producer (void * arg) {
	while(1) {
		pthread_mutex_lock(&mutex);

		while (count == buff_size)
			pthread_cond_wait(&empty, &mutex);

		put(rand() % 10);

		pthread_cond_signal(&full);
		pthread_mutex_unlock(&mutex);
	}
}

void *consumer (void * arg) {
	while(1) {
		pthread_mutex_lock(&mutex);

		while (count == 0)
			pthread_cond_wait(&full, &mutex);

		get();

		pthread_cond_signal(&empty);
		pthread_mutex_unlock(&mutex);
	} 
}

...

Why are we proving deadlock freedom?

It is a great demo for different proof techniques. The idea is simple, but the algorithm (and implementations) is easy to get wrong. The concept of concurrency is challenging for humans to get right. However, the demise of Moore's law means that algorithms have to become concurrent to keep up with growing workloads. Thus, verification pays off in this area, especially so because concurrency bugs tend to manifest in unexpected/unpredictable behavior.

A proof of deadlock-freedom is going to be small enough to be (mostly) grokkable by Formal Methods outsiders, while being complex enough to differentiate the ways we prove code correct.

I want to contribute!

We'd love to have you! Please read the contribution guidelines and then submit your favorite proofs!


以上所述就是小编给大家介绍的《Let's Prove A Concurrent Blocking Queue (sequel of Let's Prove Leftpad)》,希望对大家有所帮助,如果大家有任何疑问请给我留言,小编会及时回复大家的。在此也非常感谢大家对 码农网 的支持!

查看所有标签

猜你喜欢:

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

プログラミングコンテストチャレンジブック

プログラミングコンテストチャレンジブック

秋葉 拓哉、岩田 陽一、北川 宜稔 / 毎日コミュニケーションズ / 2010-09-11 / JPY 34.44

現在、プログラミングコンテストは数多く開催されています。Google Code Jam、TopCoder、ACM/ICPCなどの名前を聞いたことがある人も少なくないでしょう。本書で扱うのはそれらのような、問題を正確にできるだけ多く解くことを競うプログラミングコンテストです。 プログラミングコンテストは気軽に参加することができます。例えば、Google Code JamやTopCoderはイン......一起来看看 《プログラミングコンテストチャレンジブック》 这本书的介绍吧!

JSON 在线解析
JSON 在线解析

在线 JSON 格式化工具

在线进制转换器
在线进制转换器

各进制数互转换器

MD5 加密
MD5 加密

MD5 加密工具