{"id":182606,"date":"2008-04-08T00:00:00","date_gmt":"2009-10-31T09:48:35","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/a-compositional-method-for-verifying-software-transactional-memory\/"},"modified":"2024-10-02T08:49:35","modified_gmt":"2024-10-02T15:49:35","slug":"a-compositional-method-for-verifying-software-transactional-memory","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/a-compositional-method-for-verifying-software-transactional-memory\/","title":{"rendered":"A Compositional Method for Verifying Software Transactional Memory"},"content":{"rendered":"
\n

We present a method for verifying software transactional memory (STM) implementations. We decompose the problem by viewing STM descriptions at two levels: algorithm-level descriptions and actual implementations. The proof of serializability of the algorithm-level description, which is generic and performed manually, is separated from the proof that the implementation is a correct refinement of the algorithm-level description, which is checked mechanically.<\/p>\n

In the algorithm-level proof for a lazy-invalidate, write-in-place STM, we model a program composed with an abstract STM, and devise a sufficient condition for serializability expressed as three intuitive properties. The implementation-level proof consists of checking whether these properties are satisfied by the STM implementation. We were able to express each check as an assertion in a particular *sequential* program that mimics interference between threads. This is a key benefit, as it allowed the assertion checks to be carried out using the sequential program verifier Boogie. We demonstrated our approach on a model of the Bartok STM.<\/p>\n

Noteworthy additional work since the August 2007 MSR talk on this project includes the following:<\/p>\n

    \n
  1. A formal, algorithm-level model and semantics for programs using transactions. This model handles nested transactions, conflicts and rollbacks.<\/li>\n
  2. The definition of “pure serializability”, a correctness criterion for the kinds of programs described in (i).<\/li>\n
  3. A lower-level semantics that is at the same level of granularity as the actual STM implementation. This semantics also describes STM implementation state transitions that are invisible to the programmer.<\/li>\n
  4. A formalization of the desired relationship between implementation-level and algorithm-level executions. This includes translating sufficient conditions expressed at the algorithm-level to requirements at the implementation level.<\/li>\n
  5. The identification of abstractions in modeling required to make the refinement proof and algorithm-level serializability proof go through.<\/li>\n<\/ol>\n<\/div>\n

    <\/p>\n","protected":false},"excerpt":{"rendered":"

    We present a method for verifying software transactional memory (STM) implementations. We decompose the problem by viewing STM descriptions at two levels: algorithm-level descriptions and actual implementations. The proof of serializability of the algorithm-level description, which is generic and performed manually, is separated from the proof that the implementation is a correct refinement of the […]<\/p>\n","protected":false},"featured_media":194703,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_hide_image_in_river":0,"footnotes":""},"research-area":[13560],"msr-video-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-session-type":[],"msr-impact-theme":[],"msr-pillar":[],"msr-episode":[],"msr-research-theme":[],"class_list":["post-182606","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/iAvY03ddpQ0","msr_secondary_video_url":"","msr_video_file":"http:\/\/0","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/182606","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/182606\/revisions"}],"predecessor-version":[{"id":1089693,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/182606\/revisions\/1089693"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/194703"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=182606"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=182606"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=182606"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=182606"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=182606"},{"taxonomy":"msr-session-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-session-type?post=182606"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=182606"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=182606"},{"taxonomy":"msr-episode","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-episode?post=182606"},{"taxonomy":"msr-research-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-theme?post=182606"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}