Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems? 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)?
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