Aarhus University Seal / Aarhus Universitets segl

A separation logic to verify termination of busy-waiting for abrupt program exit

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearch

DOI

  • Tobias Reinhard, KU Leuven
  • ,
  • Amin Timany
  • Bart Jacobs, KU Leuven

Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approximate (i) arbitrary waitable events by abrupt program termination and (ii) busy-waiting for events by busy-waiting to be abruptly terminated. We propose a separation logic for modularly verifying termination (under fair scheduling) of programs where some threads eventually abruptly terminate the program, and other threads busy-wait for this to happen.

Original languageEnglish
Title of host publicationFTfJP 2020: Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs
Number of pages7
Place of publicationNew York
PublisherAssociation for Computing Machinery
Publication yearJul 2020
Pages26-32
ISBN (print)978-1-4503-8186-4
DOIs
Publication statusPublished - Jul 2020
Event22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020 - Virtual, Online, United States
Duration: 23 Jul 2020 → …

Conference

Conference22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020
LandUnited States
ByVirtual, Online
Periode23/07/2020 → …
SponsorACM SIGPLAN

Bibliographical note

Publisher Copyright:
© 2020 ACM.

Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.

    Research areas

  • Busy-Waiting, Separation Logic, Termination

See relations at Aarhus University Citationformats

ID: 210848956