Oct 22, 2013: Afshin Amighi: Resource Protection using Atomic operations

October 22, 2013Resource Protection using Atomic operations
Room: HalB 2FAfshin Amighi

For the verification of concurrent programs, it is essential to be able to reason about the different synchronisation mechanisms employed. As one common way to implement such synchronisation mechanisms is by means of atomic operations, we need a way to specify and reason about implementations using atomic operations.

In this talk, we use the concurrent separation logic rule for atomic operations to derive specifications for the basic atomic operations, and we instantiate our specifications for the AtomicInteger class from the java.util.concurrency library.