The semantics of blocking and nonblocking send and receive primitives

Current message-passing parallel computers provide send and receive primitives with a wide variety of blocking, synchronization, selectivity and ordering properties. Unfortunately, the interactions between the different properties of the send and receive primitives can be extremely complex, and as a result, the precise semantics of these primitives are not well understood. In 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