Mechanized Verification of Fine-grained Concurrent Programs: PLDI'15 Video Abstract
Video abstract for the paper "Mechanized Verification of Fine-grained Concurrent Programs", to appear at the 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI'15) in Portland, OR, on June 15, 2015. Inspired by Saul Goodman commercial: https://www.youtube.com/watch?v=lyEvyiyAPnA ------------------------------------------------------------------------------------- A Message about Verified Concurrency Oh, hello. I was just working on a correctness proof for a highly-scalable concurrent data structure. I know, what you're thinking: "Yeah, proving correctness sounds good, but ... what can I verify?" What can YOU verify?! Try: simple spin-lock ticketed lock abstract lock lock-based counter lock-based allocator lock-free allocator lock-free atomic snapshot lock-based stack lock-free Treiber stack sequential stack universal constructions universal construction-based stack other concurrent containers concurrent producer concurrent consumer producer/consumer composition lock-free graph manipulation The possibilities a limitless! "But, guys, how can I verify all these data structures and algorithms? I have no tools!" Do us a favour. Let us answer this question in our presentation and come to my talk!
Video abstract for the paper "Mechanized Verification of Fine-grained Concurrent Programs", to appear at the 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI'15) in Portland, OR, on June 15, 2015. Inspired by Saul Goodman commercial: https://www.youtube.com/watch?v=lyEvyiyAPnA ------------------------------------------------------------------------------------- A Message about Verified Concurrency Oh, hello. I was just working on a correctness proof for a highly-scalable concurrent data structure. I know, what you're thinking: "Yeah, proving correctness sounds good, but ... what can I verify?" What can YOU verify?! Try: simple spin-lock ticketed lock abstract lock lock-based counter lock-based allocator lock-free allocator lock-free atomic snapshot lock-based stack lock-free Treiber stack sequential stack universal constructions universal construction-based stack other concurrent containers concurrent producer concurrent consumer producer/consumer composition lock-free graph manipulation The possibilities a limitless! "But, guys, how can I verify all these data structures and algorithms? I have no tools!" Do us a favour. Let us answer this question in our presentation and come to my talk!