<p>There has been various brand of work for formalizing such tricky code. The one I know about are (but I'm no expert on the topic):</p>

<ul>
<li><p>using "temporal logic" to study distributed systems; one important tool beeing the <a href="http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html">TLA+</a> tool is a program that verifies properties of specifications expressed in temporal logic; googling for "TLA+ dining philosopher" links to <a href="http://www.cs.utah.edu/formal_verification/pdf/rpalmer_dissertation.pdf">this 2007 PhD thesis (PDF)</a> that has a TLA specification of the dining philosophers on page 24</p></li>
<li><p>using "concurrent separation logic" to verify <em>implementation</em> of concurrent programs, including rather low-level primitives. See for example the 2014 paper <a href="http://www.mpi-sws.org/~dreyer/papers/gps/paper.pdf">GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation</a> by  Aaron Turon, Viktor Vafeiadis and Derek Dreyer has correctness proofs for lock-free queues, circular buffers and "ticket locks", implemented in C using the C11 atomic concurrency pri</p></li>
</ul>

CC BY-SA 3.0
2014-06-24T20:43:20.233Z
2014-06-24T20:43:20.233Z
gasche
<p>there is a classic reference/framework increasingly standardized: </p>

<ul>
<li>C.A.R Hoare, <a href="http://www.usingcsp.com/" rel="nofollow">Communicating Sequential Processes</a> </li>
<li>a <a href="http://www.usingcsp.com/cspbook.pdf" rel="nofollow">1985 book</a> of same title is now available as ebook with open copyright. </li>
<li><a href="http://en.wikipedia.org/wiki/Communicating_sequential_processes" rel="nofollow">wikipedia</a> also has a decent overview</li>
<li>note it has some similarity/resemblance to unix <a href="http://en.wikipedia.org/wiki/Unix_Pipes" rel="nofollow">pipes/filters</a></li>
<li>there is an implementation in Java, <a href="http://en.wikipedia.org/wiki/JCSP" rel="nofollow">JCSP</a> by <a href="http://www.cs.kent.ac.uk/projects/ofa/jcsp/" rel="nofollow">Welch/Brown</a> &amp; other languages also.</li>
</ul>

CC BY-SA 3.0
2014-06-27T18:59:51.743Z
the basic idea is that using the framework, all basic parallel design patterns are supported and the system is proved formally correct & guaranteed free of common threading issues namely deadlock, livelock, race conditions, etc
vzn
CC BY-SA 3.0
2014-06-25T21:33:28.750Z
2014-06-25T21:33:28.750Z
vzn
<p>I've been going over some material related to IPC recently from Tanenbaum's "Modern Operating Systems" and revisited semaphore after many years. There is a lot of code and pseudo code based explanations and solutions to classic IPC problems like dining philosophers etc and scenario based deadlock situations.</p>

<p>However, I didn't come across any reference to proving the correctness of those solutions. I had a look at Dijkstra's original paper (following a link on Wikipedia reference section). I did a quick run through and found the explanations to be more code and pseudo code based that mathematically rigorous. The google results at best give simulation cases, which are again code based.</p>

<p>My question is as the title says: Are there any mathematically rigorous analyses and proofs about the correctness of the solutions to the IPC problems available, freely (without membership to access information)?</p>

CC BY-SA 3.0
2014-06-28T13:54:31.557Z
Note: I'll not mark a reply as "accepted" for a while so as to not discourage others from posting their alternatives. I'd up vote the replies ASAP in appreciation of the effort though. Hope this set up is alright.
vin
<pl.programming-languages><dc.parallel-comp><concurrency><formal-methods><correctness>
Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems?
vin
# Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems?

(Asked by: username_0 on 2014-06-23)

I've been going over some material related to IPC recently from Tanenbaum's "Modern Operating Systems" and revisited semaphore after many years. There is a lot of code and pseudo code based explanations and solutions to classic IPC problems like dining philosophers etc and scenario based deadlock situations.

However, I didn't come across any reference to proving the correctness of those solutions. I had a look at Dijkstra's original paper (following a link on Wikipedia reference section). I did a quick run through and found the explanations to be more code and pseudo code based that mathematically rigorous. The google results at best give simulation cases, which are again code based.

My question is as the title says: Are there any mathematically rigorous analyses and proofs about the correctness of the solutions to the IPC problems available, freely (without membership to access information)?

**Tags:** pl.programming-languages, dc.parallel-comp, concurrency, formal-methods, correctness
> **Comments:**
> **username_0**: Note: I'll not mark a reply as "accepted" for a while so as to not discourage others from posting their alternatives. I'd up vote the replies ASAP in appreciation of the effort though. Hope this set up is alright.  

---

## 2 answers

### Answer by username_1 on 2014-06-24. Score: 7

There has been various brand of work for formalizing such tricky code. The one I know about are (but I'm no expert on the topic):

* using "temporal logic" to study distributed systems; one important tool beeing the [TLA+](http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html) tool is a program that verifies properties of specifications expressed in temporal logic; googling for "TLA+ dining philosopher" links to [this 2007 PhD thesis (PDF)](http://www.cs.utah.edu/formal_verification/pdf/rpalmer_dissertation.pdf) that has a TLA specification of the dining philosophers on page 24
* using "concurrent separation logic" to verify *implementation* of concurrent programs, including rather low-level primitives. See for example the 2014 paper [GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation](http://www.mpi-sws.org/~dreyer/papers/gps/paper.pdf) by Aaron Turon, Viktor Vafeiadis and Derek Dreyer has correctness proofs for lock-free queues, circular buffers and "ticket locks", implemented in C using the C11 atomic concurrency pri


---

### Answer by username_2 on 2014-06-25. Score: 2

there is a classic reference/framework increasingly standardized:

* C.A.R Hoare, [Communicating Sequential Processes](http://www.usingcsp.com/)
* a [1985 book](http://www.usingcsp.com/cspbook.pdf) of same title is now available as ebook with open copyright.
* [wikipedia](http://en.wikipedia.org/wiki/Communicating_sequential_processes) also has a decent overview
* note it has some similarity/resemblance to unix [pipes/filters](http://en.wikipedia.org/wiki/Unix_Pipes)
* there is an implementation in Java, [JCSP](http://en.wikipedia.org/wiki/JCSP) by [Welch/Brown](http://www.cs.kent.ac.uk/projects/ofa/jcsp/) & other languages also.

> **Comments:**
> **username_2**: the basic idea is that using the framework, all basic parallel design patterns are supported and the system is proved formally correct & guaranteed free of common threading issues namely deadlock, livelock, race conditions, etc  

---

