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.