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.

http://goo.gl/GFwDVY

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s