Explanation of two non-blocking shared-variable communication algorithms

Article


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
TypeArticle
TitleExplanation of two non-blocking shared-variable communication algorithms
AuthorsBornat, R. and Amjad, H.
Abstract

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
ISSN0934-5043
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
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/842q2

  • 22
    total views
  • 0
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as

Related outputs

Describing and simulating concurrent quantum systems
Bornat, R., Boender, J., Kammueller, F., Poly, G. and Nagarajan, R. 2020. Describing and simulating concurrent quantum systems. Biere, A. and Parker, D. (ed.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 20). Dublin 27 - 30 Apr 2020 Springer. pp. 271-277 https://doi.org/10.1007/978-3-030-45237-7_16
New lace and arsenic: adventures in weak memory with a program logic (v2)
Bornat, R., Alglave, J. and Parkinson, M. 2016. New lace and arsenic: adventures in weak memory with a program logic (v2). arXiv.org arXiv. https://doi.org/10.48550/arXiv.1512.01416
Towards automatic stability analysis for rely-guarantee proofs
Amjad, H. and Bornat, R. 2009. Towards automatic stability analysis for rely-guarantee proofs. in: Jones, N. and Müller-Olm, M. (ed.) Verification, model checking, and abstract interpretation: 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings Springer.
Separation logic and concurrency
Bornat, R. 2010. Separation logic and concurrency. in: Boca, P., Bowen, J. and Siddiqi, J. (ed.) Formal Methods: State of the Art and New Directions London Springer Verlag. pp. 217-248
Inter-process buffers in separation logic with rely-guarantee
Bornat, R. and Amjad, H. 2010. Inter-process buffers in separation logic with rely-guarantee. Formal Aspects of Computing. 22 (6), pp. 735-772. https://doi.org/10.1007/s00165-009-0141-8
Cyclic proofs of program termination in separation logic
Brotherston, J., Bornat, R. and Calcagno, C. 2008. Cyclic proofs of program termination in separation logic. ACM SIGPLAN Notices - POPL '08. 43 (1), pp. 101-112. https://doi.org/10.1145/1328897.1328453
Variables as resource in Hoare logic.
Bornat, R., Calcagno, C. and Parkinson, M. 2006. Variables as resource in Hoare logic. in: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, Washington. Proceedings. IEEE Computer Society. pp. 137-146
Variables as resources in separation logic.
Bornat, R., Calcagno, C. and Yang, H. 2006. Variables as resources in separation logic. 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), Birmingham, UK. Proceedings in Electronic Notes in Theoretical Computer Science. Elsevier B.V.. 155, pp. 247-276. https://doi.org/10.1016/j.entcs.2005.11.059
Modular verification of a non-blocking stack.
Bornat, R., Parkinson, M. and O'Hearn, P. 2007. Modular verification of a non-blocking stack. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '07), Nice, France. Proceedings.. https://doi.org/10.1145/1190216.1190261
Permission accounting in separation logic.
Bornat, R., Calcagno, C., Parkinson, M. and O'Hearn, P. 2005. Permission accounting in separation logic. 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '05), Long Beach, California, USA. Proceedings. https://doi.org/10.1145/1047659.1040327