Semantics of blocking and nonblocking send and receive primitives

Abstract

This paper we present formal models for message-passing systems that provide both synchronous and asynchronous sends, both blocking and nonblocking sends and receives, and a variety of ordering properties. In addition, the receive primitives are very general in that they can specify the desired source and/or tag value of a message. Our models apply to all message-passing programs, including ones with errors, and they apply to parallel computers with arbitrary amounts of buffering. To the best of our knowledge, this is the first time that such rich message-passing models have been defined formally. In addition to presenting the formal models, we also give a number of theorems that capture the properties of the models.