An Operational Semantics for Shared Messaging Communication

Shared Messaging Communication (SMC) has been introduced in [9] as a model of communication which reduces communication costs (both in terms of communication latency and memory usage) by allowing tasks to communicate data through special shared memory regions. Sending a reference to an otherwise inaccessible memory regions rather than the data itself, the model combines the advantages of message passing and shared memories. Experimental results have shown that SMC in case of large data payloads clearly outperforms the classical message passing. In this paper we give a formal operational semantics to SMC exhibiting unambiguously the effect of executing an SMC command on local and shared memories. Based on this semantics we show that any program using message passing can be proved to be weakly bisimilar to one based on SMC and that with respect to communication costs the latter is amortised cheaper, [7]