Wed 10 Jan 2018 17:05 - 17:30 at Bunker Hill - Memory and Concurrency Chair(s): Azadeh Farzan

Various progress properties have been proposed for concurrent objects, such as wait-freedom, lock-freedom, starvation-freedom and deadlock-freedom. However, none of them apply for concurrent objects with partial methods, i.e. methods that are supposed not to return under certain circumstances. A typical example is the lock_acquire method.

In this paper we propose two new progress properties, partial starvation-freedom (PSF) and partial deadlockfreedom (PDF), for concurrent objects with partial methods. We also design four patterns to write abstract specifications for PSF or PDF objects under strongly or weakly fair scheduling, so that these objects contextually refine the abstract specifications. Our Abstraction Theorem shows the equivalence between PSF (or PDF) and the progress-aware contextual refinement. Finally, we generalize the program logic LiLi to have a new logic to verify the PSF or PDF property and linearizability of concurrent objects.

Wed 10 Jan
Times are displayed in time zone: Tijuana, Baja California change

15:50 - 17:30: Memory and ConcurrencyResearch Papers at Bunker Hill
Chair(s): Azadeh FarzanUniversity of Toronto
15:50 - 16:15
Effective Stateless Model Checking for C/C++ Concurrency
Research Papers
Michalis KokologiannakisNational Technical University of Athens, Greece, Ori LahavTel Aviv University, Israel, Konstantinos (Kostis) Sagonas, Viktor VafeiadisMPI-SWS, Germany
16:15 - 16:40
Transactions in Relaxed Memory Architectures
Research Papers
Brijesh DongolBrunel University London, Radha JagadeesanDePaul University, James RielyDePaul University
Link to publication DOI Pre-print Media Attached
16:40 - 17:05
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Research Papers
Christopher PulteUniversity of Cambridge, Shaked FlurUniversity of Cambridge, Will DeaconARM Ltd., Jon FrenchUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, Peter SewellUniversity of Cambridge
17:05 - 17:30
Progress of Concurrent Objects with Partial Methods
Research Papers
Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China