[talks] Nick Giannarakis will present his general exam on January 24, 2017 at 9:30am in CS 302.

[Nicki Gotsis]

Nick Giannarakis will present his general exam on January 24, 2017 at 9:30am in CS 302. The members of his committee are: Andrew Appel (adviser), Margaret Martonosi, and David Walker. 

Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. 

Title: Semantics of well synchronized programs on weakly consistent machines. 

Abstract: 
The semantics of shared-memory concurrent programs are quite intricate. For one, optimizing compilers perform transformations that may be unsound with respect to concurrent programs. Moreover, modern multiprocessors have relaxed semantics: the widespread assumption of sequential consistency is invalidated by common architectural optimizations. Processors reorder instructions (or executes them out of order), and techniques such as caching of memory data and buffering of operations break the abstraction of a single global view of the memory shared by all threads. Programs that don’t have data races, however, should execute as if they were running on a sequentially consistent machine. 
In this work, we focus on a class of programs called well synchronized; access to some part of the shared memory is arbitrated by synchronizing operations and threads do not compete with each other for that memory. Using the Coq proof assistant, we formalized this notion of well synchronized programs, and used it to prove that cooperative (yield on synchronizing operations) and preemptive (interleaving) semantics of such programs coincide. Furthermore, we proved that well synchronized programs don’t have data races, hence their relaxed semantics coincides with their interleaving semantics. 
We prove that result in a generic and modular way, and demonstrate its applicability on the TSO memory model using the X86 ISA. 

Reading List: 
• Stability in weak memory models, Jade Alglave, Luc Maranget. In CAV 2010. 
• Relaxed Memory Concurrency and Verified Compilation. Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell. In POPL 2011. 
• Reasoning about the Implementation of Concurrency Abstractions on x86-TSO, Scott Owens. In ECOOP 2010. 
• Compositional CompCert. Gordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel. In POPL 2015. 
• Taming Weak memory models.Sizhuo Zhang, Arvind, Muralidaran Vijayaraghavan. Draft. 
• Verifying read-copy-update in a logic for weak memory. Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis. In PLDI 2015. 
• A promising semantics for relaxed-memory concurrency. Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer. In POPL 2017. 
• Types and Programming Languages, Benjamin C. Pierce. 
• The Formal Semantics of Programming Languages, Glynn Winskel. 





-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.cs.princeton.edu/pipermail/talks/attachments/20170118/8edbbdb5/attachment.html>