Blogs (2) >>
ISMM 2017
Sun 18 Jun 2017 Barcelona, Spain
co-located with PLDI 2017
Sun 18 Jun 2017 16:30 - 17:00 at Aula Master - Session 4: A Deeper Look Chair(s): Steve Blackburn

Existing implementations of dynamic memory allocators (DMA) employ a large spectrum of policies and techniques. The formal specifications of these techniques are quite complicated in isolation and very complex when combined. Therefore, the formal reasoning on a specific DMA implementation is difficult for automatic tools and mostly single-use. This paper proposes a solution to this problem by providing formal models for a full class of DMA, the free list class. To obtain manageable formal reasoning and reusable formal models, we organise these models in a hierarchy ranked by refinement relations. We prove the soundness of models and refinement relations using an off-the-shelf theorem prover. We demonstrate that our hierarchy is a basis for an algorithm theory for the class of free list DMA: it abstracts various existing implementations of DMA and leads to new DMA implementations. We illustrate its application to model-based code generation, testing, run-time verification, and static analysis.

Conference Day
Sun 18 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Session 4: A Deeper LookISMM 2017 at Aula Master
Chair(s): Steve BlackburnAustralian National University
16:00
30m
Talk
"What's in a Name?" Going Beyond Allocation Site Names in Heap Analysis
ISMM 2017
Vini KanvarIndian Institute of Technology (IIT) Bombay, Uday P. Khedker
16:30
30m
Talk
A Refinement Hierarchy for Free List Memory Allocators
ISMM 2017
Bin FangEast China Normal University (China) and University Paris Diderot and CNRS (France), Mihaela SighireanuIRIF, University Paris Diderot and CNRS, France
17:00
30m
Talk
Avoiding Consistency Exceptions Under Strong Memory Consistency Models
ISMM 2017
Minjia ZhangMicrosoft Research, Swarnendu BiswasUniversity of Texas at Austin, Michael D. BondOhio State University