Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research
Final published version
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 language | English |
---|---|
Title of host publication | FTfJP 2020: Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs |
Number of pages | 7 |
Place of publication | New York |
Publisher | Association for Computing Machinery |
Publication year | Jul 2020 |
Pages | 26-32 |
ISBN (print) | 978-1-4503-8186-4 |
DOIs | |
Publication status | Published - Jul 2020 |
Event | 22nd 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 | 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020 |
---|---|
Land | United States |
By | Virtual, Online |
Periode | 23/07/2020 → … |
Sponsor | ACM SIGPLAN |
Publisher Copyright:
© 2020 ACM.
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
See relations at Aarhus University Citationformats
ID: 210848956