Synchronous Message Passing and Semaphores: An Equivalence Proof

A natural encoding of synchronous message exchange with direct wait-control is proved to be equivalent in a distributed environment to a refinement which uses semaphores to implement wait control. The proof uses a most general scheduler, which is left as abstract and assumed to satisfy a few realistic, explicitly stated assumptions. We hope to provide a scheme that can be implemented by current theorem provers.

• Type: Conference
• Year: 2010
• Where: ASM
• Authors: Iain Craig, Egon Börger
• Keywords: ASM 2010, Current Theorem Provers, Microbiology, Natural Encoding, Synchronous Message Exchange