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