New Meetup: Reasoning on transactional programming

Verifying Programs under Snapshot Isolation and Similar Relaxed Consistency Model

In this talk, I will present a static verification approach for programs running under snapshot isolation (SI) and similar relaxed transactional semantics. Relaxed conflict detection schemes such as snapshot isolation (SI) are used widely. Under SI, transactions are no longer guaranteed to be serializable, and the simplicity of reasoning sequentially within a transaction is lost. In this paper, we present an approach for statically verifying properties of transactional programs operating under SI. Differently from earlier work, we handle transactional programs even when they are designed not to be serializable.

I will present a source-to-source transformation which augments the program with an encoding of the SI semantics. Verifying the resulting program with transformed user annotations and specifications is equivalent to verifying the original transactional program running under SI — a fact we prove formally. Encoding which I present preserves the modularity and scalability of VCC’s verification approach. I will show the application of the method successfully to benchmark programs from the transactional memory literature.

by İsmail Kuru

PS: Time and Place will be determined in related with participant count and suggestions.

Not: Şimdilik yer ve zaman konusu net değil. Katılımcı sayısı ve istekleri doğrultusunda kesin olarak karar verilecektir.