5
$\begingroup$

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)?

Improve this question
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – vin
    Commented Jun 28, 2014 at 13:54

2 Answers 2

Reset to default
7
$\begingroup$

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+ 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) 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 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

Improve this answer
$\endgroup$
2
$\begingroup$

there is a classic reference/framework increasingly standardized:

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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 $\endgroup$
    – vzn
    Commented Jun 27, 2014 at 18:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.