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)》,希望对大家有所帮助,如果大家有任何疑问请给我留言,小编会及时回复大家的。在此也非常感谢大家对 码农网 的支持!

查看所有标签

猜你喜欢:

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

PYTHON3:数据分析与机器学习实战

PYTHON3:数据分析与机器学习实战

龙马高新教育 / 北京大学出版社 / 2018-9-1 / 69.00

机器学习(Machine Learning, ML)是一门多领域交叉学科,是人工智能的核心,其应用遍及人工智能的各个领域,专门研究计算机怎样模拟或实现人类的学习行为,以获取新的知识或技能,重新组织已有的知识结构使之不断改善自身的性能。在机器学习过程中,需要使用大量数据,而数据分析是指用适当的方法对收集的大量数据进行分析,提取有用信息并形成结论,进而对数据加以详细研究和概括总结的过程。本书结合机器学......一起来看看 《PYTHON3:数据分析与机器学习实战》 这本书的介绍吧!

JS 压缩/解压工具
JS 压缩/解压工具

在线压缩/解压 JS 代码

图片转BASE64编码
图片转BASE64编码

在线图片转Base64编码工具

SHA 加密
SHA 加密

SHA 加密工具