This talk argues that exposing inherent limitations of synchronization can positively affect the design and verification of concurrent programs. This is demonstrated with two examples: The first result shows that, for a large class of objects, any implementation must include specific, easy-to-detect patterns of memory accesses. The second is a reduction theorem showing that many locking protocols need only be verified in a sequential setting.
The talk is based on work that appeared in POPL 2010 and POPL 2011.
Hagit Attiya is a professor at the department of Computer Science at the Technion, Israel Institute of Technology, and holds the Harry W. Labov and Charlotte Ullman Labov Academic Chair. She received the B.Sc. degree in Mathematics and Computer Science from The Hebrew University of Jerusalem, in 1981, the M.Sc. and Ph.D. degrees in Computer Science from the Hebrew University of Jerusalem, in 1983 and 1987, respectively. Before joining the Technion, she has been a post-doctoral research associate at the Laboratory for Computer Science at M.I.T.
Her research interests are in distributed and parallel computing.
She is the editor-in-chief for Springer's journal Distributed Computing and a fellow of the ACM.
