To drive the proof system and tool design, we have been using a new concurrent mark-sweep garbage collector we developed that will become part of the Ironclad verified OS. The top-level functional specification for the garbage collector is to appear invisible to application threads. We explain how we refine this top-level specification down to a concurrent implementation described at the level of individual memory accesses. We highlight challenges we encountered while carrying out a proof spanning such a large abstraction gap and how features of our proof system help us address them.

Joint work with Erez Petrank (Technion), Chris Hawblitzel, and Shaz Qadeer (Microsoft Research)

Serdar Tasiran received his PhD from UC Berkeley in 1998. He was a research scientist at the DEC/Compaq/HP Systems Research Center (SRC) until 2003. Since then, he has been a professor at Koc University, Istanbul, Turkey. He has received the Turkish Academy of Sciences Distinguished Young Scientist Award. He has had visiting appointments at MIT, EPFL, Microsoft Research, USA, UK, and India. He is a member of the IFIP Working Group 2.3 on Programming Methodology and a member of the ACM Europe Council. He collaborates closely with Microsoft Research and has spent six months of his sabbatical leave at MSR Redmond in the RiSE group and three months at MSR Cambridge. He will be visiting LIP6 for the next two months.