Explanation of two non-blocking shared-variable communication algorithms


Bornat, R. and Amjad, H. 2011. Explanation of two non-blocking shared-variable communication algorithms. Formal Aspects of Computing. https://doi.org/10.1007/s00165-011-0213-4
TitleExplanation of two non-blocking shared-variable communication algorithms
AuthorsBornat, R. and Amjad, H.

Simpson and Harris have described multi-slot algorithms implementing a single-place buffer, each operating without explicit hardware synchronisation mechanisms. Conventional refinement and proof techniques have explained that these algorithms work, but do not give convincing descriptions of how they work. An unconventional refinement process starting from the classic single-variable buffer, using both data and atomicity refinement and drawing information from unsuccessful steps, derives each algorithm. The logic used is RGSep, a marriage of rely/guarantee and concurrent separation logic. Extensive detailed verifications are described. The result is an explanation of how the algorithms work and some pointers to how such algorithms might be devised.

KeywordsSeparation logic, Rely-guarantee, Concurrency, Proof, Refinement, Atomicity,
Research GroupFoundations of Computing group
PublisherSpringer Verlag
JournalFormal Aspects of Computing
Publication dates
PrintDec 2011
Publication process dates
Deposited03 Jul 2013
Output statusPublished
Digital Object Identifier (DOI)https://doi.org/10.1007/s00165-011-0213-4
Permalink -


  • 17
    total views
  • 0
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as