{"id":167948,"date":"2015-06-01T00:00:00","date_gmt":"2015-06-01T00:00:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/asynchronous-programming-analysis-and-testing-with-state-machines\/"},"modified":"2018-10-16T20:02:42","modified_gmt":"2018-10-17T03:02:42","slug":"asynchronous-programming-analysis-and-testing-with-state-machines","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/asynchronous-programming-analysis-and-testing-with-state-machines\/","title":{"rendered":"Asynchronous Programming, Analysis and Testing with State Machines"},"content":{"rendered":"<div class=\"asset-content\">\n<p>Programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against interleaving-dependent bugs such as data races and other assertion violations. Previous work has only addressed these challenges individually, either by designing a new declarative language, or a new data race detection tool, or a new testing technique. We present P#, a language for high-reliability asynchronous programming co-designed with a static analysis and testing infrastructure. We describe our experience using P# to write several distributed protocols and port an industrial-scale system internal to Microsoft, showing that the supporting techniques, by leveraging the design of P#, are effective in finding bugs.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against interleaving-dependent bugs such as data races and other assertion violations. Previous work has only addressed these challenges individually, either by designing a new declarative language, or a new data race detection tool, or a [&hellip;]<\/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":[193716],"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-167948","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_publishername":"ACM","msr_edition":"Programming Language Design and Implementation (PLDI)","msr_affiliation":"","msr_published_date":"2015-06-01","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_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":"204323","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","title":"paper.pdf","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/paper-6.pdf","id":204323,"label_id":0}],"msr_related_uploader":"","msr_attachments":[{"id":204323,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/paper-6.pdf"}],"msr-author-ordering":[{"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":"text","value":"Pantazis Deligiannis","user_id":0,"rest_url":false},{"type":"text","value":"Alastair Donaldson","user_id":0,"rest_url":false},{"type":"text","value":"Paul Thomson","user_id":0,"rest_url":false},{"type":"text","value":"Jeroen Ketema","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[199562],"msr_event":[],"msr_group":[144939],"msr_project":[615984,239342],"publication":[],"video":[],"download":[],"msr_publication_type":"inproceedings","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&hellip;","_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\/167948","targetHints":{"allow":["GET"]}}],"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":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/167948\/revisions"}],"predecessor-version":[{"id":520072,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/167948\/revisions\/520072"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=167948"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=167948"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=167948"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=167948"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=167948"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=167948"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=167948"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=167948"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=167948"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=167948"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=167948"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=167948"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=167948"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=167948"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=167948"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=167948"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}