Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Thu 21 Jan 2021 19:10 - 19:20 at POPL-A - Complexity

Non-Volatile Random Access Memories, or Persistent Memories (PM), is an emerging technology offering both efficiency of DRAMs and persistency of data across failures. However, while they allow recovering some data, recovery states are not always consistent, and programmers must provide adequate recovery code ensuring the level of consistency they need. This task is hard and error prone, and therefore, being able to reason formally about concurrent programs running on PMs and verifying their correctness is extremely important.

In this paper, we address the problem of verifying the reachability problem in programs under the formal model Px86 defined recently by Raad et al. in POPL’20 for the persistent Intel x86 architecture. We prove that this problem is decidable. To achieve that, we provide a new formal model that is equivalent to Px86 and that has the feature of being a well-structured system. Deriving this new model is the result of a deep investigation of the properties of Px86 and the interplay of its components.

Thu 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30
ComplexityPOPL at POPL-A
18:30
10m
Talk
Learning the Boundary of Inductive Invariants
POPL
Yotam M. Y. FeldmanTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv University, James R. WilcoxUniversity of Washington
Link to publication DOI
18:40
10m
Talk
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
POPL
Andreas PavlogiannisAarhus University, Anders Alnor MathiasenAarhus University
Link to publication DOI
18:50
10m
Talk
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory ProgramsDistinguished Paper
POPL
Pascal BaumannMax Planck Institute for Software Systems (MPI-SWS), Rupak MajumdarMPI-SWS, Ramanathan S. ThinniyamMax Planck Institute for Software Systems (MPI-SWS), Georg ZetzscheMax Planck Institute for Software Systems (MPI-SWS)
Link to publication DOI
19:00
10m
Talk
Deciding ω-Regular Properties on Linear Recurrence Sequences
POPL
Shaull AlmagorTechnion, Toghrul KarimovMax Planck Institute for Software Systems, Edon KelmendiUniversity of Oxford, Joël OuaknineMax Planck Institute for Software Systems and University of Oxford, James WorrellUniversity of Oxford
Link to publication DOI
19:10
10m
Talk
Deciding Reachability under Persistent x86-TSO
POPL
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Ahmed BouajjaniIRIF, Université Paris Diderot, K Narayan KumarChennai Mathematical Institute, Prakash SaivasanThe Institute of Mathematical Sciences, India
Link to publication DOI
19:20
10m
Talk
On the Complexity of Bidirected Interleaved Dyck-Reachability
POPL
Yuanbo LiGeorgia Institute of Technology, USA, Qirun ZhangGeorgia Institute of Technology, USA, Thomas RepsUniversity of Wisconsin--Madison
Link to publication DOI