POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

Modern processors such as ARMv8 and RISC-V allow executions in which independent instructions within a process may be re-ordered. To cope with such phenomena, so called promising semantics have been developed, which permit threads to read values that have not yet been written. Each promise is a speculative update that is later validated (fulfilled) by an actual write. Promising semantics are operational, providing a pathway for developing proof calculi. In this paper, we develop an incorrectness-style logic, resulting in a framework for reasoning about state reachability. Like incorrectness logic, our assertions are underapproximating, since the set of all valid promises are not known at the start of execution. Our logic uses event structures as assertions to compactly represent the ordering among events such as promised and fulfilled writes.

Tue 16 Jan

Displayed time zone: London change

14:00 - 15:30
Concurrency, Security, & Hyper-propertiesIncorrectness at Mountbatten Exhibition
Chair(s): Azalea Raad Imperial College London
14:00
22m
Talk
Quantitative Weakest Hyper Pre
Incorrectness
Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University; University College London
File Attached
14:22
23m
Talk
A Reachability Logic for a Weak Memory Model with Promises
Incorrectness
Lara Bargmann University of Oldenburg, Brijesh Dongol University of Surrey, Heike Wehrheim University of Oldenburg
File Attached
14:45
22m
Talk
Towards Temporal Adversarial Logic
Incorrectness
Julien Vanegue Bloomberg, USA
15:07
22m
Talk
Finding counterexamples to ∀∃ hyperproperties
Incorrectness
DOI Pre-print