We study the problem of finding liveness violations in real-world
\nasynchronous distributed systems. Unlike a safety property, which
\nasserts that certain bad states should never occur during execution, a
\nliveness property states that a program should not remain in a bad
\nstate for an infinitely long period of time. Checking for liveness
\nviolations is an essential testing activity to ensure that a system
\nwill always make progress in production.<\/p>\n
The violation of a liveness property can be demonstrated by a finite
\nexecution where the same system state repeats twice (known as
\nlasso). However, this requires the ability to capture the state
\nprecisely, which is arguably impossible in real-world systems. For
\nthis reason, previous approaches have instead relied on demonstrating
\na long execution where the system remains in a bad state. However,
\nthis hampers debugging because the produced trace can be very long,
\nmaking it hard to understand.<\/p>\n
Our work aims to find liveness violations in real-world systems while
\nstill producing lassos as a bug witness. Our technique relies only on
\npartially caching the system state, which is feasible to achieve
\nefficiently in practice. To make up for imprecision in caching, we use
\nretries: a potential lasso, where the same partial state repeats
\ntwice, is replayed multiple times to gain certainty that the execution
\nis indeed stuck in a bad state.<\/p>\n
We have implemented our technique in the P# programming language and
\nevaluated it on real production systems and several challenging
\nacademic benchmarks.<\/p>\n","protected":false},"excerpt":{"rendered":"
We study the problem of finding liveness violations in real-world asynchronous distributed systems. Unlike a safety property, which asserts that certain bad states should never occur during execution, a liveness property states that a program should not remain in a bad state for an infinitely long period of time. Checking for liveness violations is an […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"msr-content-type":[3],"msr-research-highlight":[],"research-area":[13560],"msr-publication-type":[193718],"msr-product-type":[],"msr-focus-area":[],"msr-platform":[],"msr-download-source":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-418130","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_publishername":"","msr_edition":"","msr_affiliation":"","msr_published_date":"2017-07-31","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"MSR-TR-2017-37","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"418517","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","title":"liveness-tr","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/07\/liveness-tr.pdf","id":418517,"label_id":0}],"msr_related_uploader":"","msr_attachments":[],"msr-author-ordering":[{"type":"text","value":"Rashmi Mudduluru","user_id":0,"rest_url":false},{"type":"user_nicename","value":"pdeligia","user_id":36200,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=pdeligia"},{"type":"text","value":"Ankush Desai","user_id":0,"rest_url":false},{"type":"user_nicename","value":"akashl","user_id":30905,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=akashl"},{"type":"user_nicename","value":"qadeer","user_id":33294,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=qadeer"}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[615984,239342],"publication":[],"video":[],"download":[],"msr_publication_type":"techreport","related_content":{"projects":[{"ID":615984,"post_title":"Coyote","post_name":"coyote","post_type":"msr-project","post_date":"2020-01-30 16:10:47","post_modified":"2022-06-29 16:22:15","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/coyote\/","post_excerpt":"Coyote provides developers a programming framework for confidently building reliable asynchronous software on the .NET platform.","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/615984"}]}},{"ID":239342,"post_title":"Safe Asynchronous Programming with P and P#","post_name":"safe-asynchronous-programming-p-p","post_type":"msr-project","post_date":"2016-06-16 18:31:15","post_modified":"2021-04-13 14:40:32","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/safe-asynchronous-programming-p-p\/","post_excerpt":"We are designing programming languages for building safe and reliable\u00a0asynchronous systems. These languages are based on the programming idiom of asynchronous communicating state machines. They offer first-class support for writing safety and liveness specifications as well as building abstract models of the code. They offer systematic testing capabilities that exhaustively (in the limit) test all possible executions of the program, weeding out hard-to-find concurrency bugs. P is a (domain-specific) programming language for modeling and specifying…","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/239342"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/418130"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/418130\/revisions"}],"predecessor-version":[{"id":418520,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/418130\/revisions\/418520"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=418130"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=418130"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=418130"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=418130"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=418130"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=418130"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=418130"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=418130"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=418130"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=418130"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=418130"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=418130"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=418130"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=418130"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=418130"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=418130"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}