Azadeh Farzan: Causal Atomicity

Abstract: Atomicity is an important generic specification that assures that a programmer can pretend that blocks occur sequentially in any execution. We define a notion of atomicity based on causality. We model the control flow of a program with threads using a Petri net that naturally abstracts data, and faithfully captures the independence and interaction between threads. The causality between events in the partially ordered executions of the Petri net is used to define the notion of causal atomicity. We show that causal atomicity is a robust notion that many correct programs adopt, and show how we can effectively check causal atomicity using Petri net tools based on unfoldings, which exploit the concurrency in the net to yield automatic partial-order reduction in the state-space.


Bio: Azadeh Farzan a post-doctoral researcher at the School of Computer Science at Carnegie-Mellon University. She earned her B.S. degree in computer engineering from Sharif University of Technology at Tehran in 2000, and her Ph.D. in computer science from University of Illinois at Urbana-Champaign in January 2007. Her research interests are in the areas of software verification, concurrency, programming languages and security.

Appointments: dcm@cs.cmu.edu


Maintainer Home > Seminar ]
`Last modified: Mon Feb 26 11:09:10 EDT 2007