Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Wed 25 Oct 2017 14:37 - 15:00 at Regency A - Gradual Types and Memory Chair(s): Jennifer B. Sartor

Modern concurrent copying garbage collection (GC), especially real-time GC, employ fine-grain synchronisations with mutators, which are application programs that mutate memory, when they move objects in their copy phases. They resolve a data-race using concurrent copying protocols, which are implemented as interactions between the collectors and the read and write barriers that the mutators execute. Behavioural effects of the concurrent copying protocol relies on the memory model of the CPUs and the programming languages in which the GC is implemented. It is hard, however, to formally investigate behavioural properties of concurrent copying protocols against various memory models.

To address this problem, we studied the feasibility of bounded model checking of concurrent copying protocols with memory models. We investigated a correctness-related behavioural property of copying protocols of various concurrent copying GC algorithms including real-time GC Stopless, Clover, Chicken, Staccato, and Schism against six memory models, TSO, PSO, RMO, and their variants as well as sequential consistency by using bounded model checking. For each combination of a protocol and a memory model, we conducted model checking with a model of a mutator. In this wide range of case studies, we found faults in two GC algorithms, one of which is relevant to the memory model. We fixed these faults with great help of counterexamples. We also modified some protocols so that they works correctly under some memory models weaker than the ones that the original protocols are designed for, and checked them by using model checking. We believe that bounded model checking is a feasible approach to investigate behavioural properties of concurrent copying protocols under weak memory models.

Wed 25 Oct
Times are displayed in time zone: Tijuana, Baja California change

13:30 - 15:00: Gradual Types and MemoryOOPSLA at Regency A
Chair(s): Jennifer B. SartorVrije Universiteit Brussel
13:30 - 13:52
Talk
Sound Gradual Typing: Only Mostly Dead
OOPSLA
Spenser Andrew BaumanIndiana University, USA, Sam Tobin-HochstadtIndiana University, Jeremy G. SiekIndiana University, USA, Carl Friedrich Bolz-Tereick
DOI
13:52 - 14:15
Talk
Sound Gradual Typing Is Nominally Alive and Well
OOPSLA
Fabian MuehlboeckCornell University, Ross TateCornell University
DOI
14:15 - 14:37
Talk
The VM Already Knew That: Leveraging Compile-Time Knowledge to Optimize Gradual Typing
OOPSLA
Gregor RichardsUniversity of Waterloo, Ellen ArtecaUniversity of Waterloo, Canada, Alexi TurcotteUniversity of Waterloo
DOI
14:37 - 15:00
Talk
Model Checking Copy Phases of Concurrent Copying Garbage Collection with Various Memory Models
OOPSLA
Tomoharu UgawaKochi University of Technology, Japan, Tatsuya AbeChiba Institute of Technology, Japan, Toshiyuki MaedaChiba Institute of Technology, Japan
DOI