Towards Formally Refining BSP Barriers into Explicit Two - Sided Communications

摘要

An experiment is conducted to assess the feasibility of transforming BSP computations into systems employing explicit asynchronous two - sided communications. The aim of the work is to show how a verified BSP program may be transformed into a guaranteed correct conventional message-passing implementation which may, in certain circumstances, avoid the expense of providing a synchronisation barrier.