P.: TaDA: A Logic for Time and Data Abstraction

Abstract. To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with lin-earisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concur-rent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources. We present TaDA, a program logic that combines the benefits of ab-stract atomicity and abstract disjointness. Our key contribution is the introduction of atomic triples, which offer an expressive approach to spec-ifying program modules. By building up examples, we show that TaDA supports elegant modular reasoning in a way that was not previously possible.