{"id":338456,"date":"1982-07-01T00:00:58","date_gmt":"1982-07-01T07:00:58","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&p=338456"},"modified":"2018-10-16T22:20:38","modified_gmt":"2018-10-17T05:20:38","slug":"proving-liveness-properties-concurrent-programs","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/proving-liveness-properties-concurrent-programs\/","title":{"rendered":"Proving Liveness Properties of Concurrent Programs"},"content":{"rendered":"

During the late 70s and early 80s, Susan Owicki and I worked together quite a bit. We were even planning to write a book on concurrent program verification. But this paper is the only thing we ever wrote together.<\/p>\n

In [23]<\/a>, I had introduced a method of proving eventuality properties of concurrent programs by drawing a lattice of predicates, where arrows from a predicate P to predicates Q1, …, Qn mean that, if the program reaches a state satisfying P, it must thereafter reach a state satisfying one of the Qi. That method never seemed practical; formalizing an informal proof was too much work.<\/p>\n

Pnueli’s introduction of temporal logic allowed the predicates in the lattice to be replaced by arbitrary temporal formulas. This turned lattice proofs into a useful way of proving liveness properties. It permitted a straightforward formalization of a particularly style of writing the proofs. I still use this proof style to prove leads-to properties, though the proofs are formalized with TLA (see [102]<\/a>). However, I no longer bother drawing pictures of the lattices. This paper also introduced at, in, and after predicates for describing program control.<\/p>\n

It’s customary to list authors alphabetically, unless one contributed significantly more than the other, but at the time, I was unaware of this custom. Here is Owicki’s account of how the ordering of the authors was determined.<\/p>\n

As I recall it, you raised the question of order, and I proposed alphabetical order. You declined–I think you expected the paper to be important and didn’t think it would be fair to get first authorship on the basis of a static property of our names. On the night we finished the paper, we went out to dinner to celebrate, and you proposed that if the last digit of the bill was even (or maybe odd), my name would be first. And, indeed, that’s the way it came out.<\/p>\n","protected":false},"excerpt":{"rendered":"

During the late 70s and early 80s, Susan Owicki and I worked together quite a bit. We were even planning to write a book on concurrent program verification. But this paper is the only thing we ever wrote together. In [23], I had introduced a method of proving eventuality properties of concurrent programs by drawing […]<\/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":"","msr-author-ordering":null,"msr_publishername":"ACM","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"ACM Transactions on Programming Languages and Systems","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"3","msr_journal":"ACM Transactions on Programming Languages and Systems","msr_number":"","msr_organization":"","msr_pages_string":"455-495","msr_page_range_start":"455","msr_page_range_end":"495","msr_series":"","msr_volume":"4","msr_copyright":"Copyright \u00a9 1982 by the Association for Computing Machinery, Inc.Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and\/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org. The definitive version of this paper can be found at ACM's Digital Library --http:\/\/www.acm.org\/dl\/.","msr_conference_name":"","msr_doi":"","msr_arxiv_id":"","msr_s2_paper_id":"","msr_mag_id":"","msr_pubmed_id":"","msr_other_authors":"","msr_other_contributors":"","msr_speaker":"","msr_award":"","msr_affiliation":"","msr_institution":"","msr_host":"","msr_version":"","msr_duration":"","msr_original_fields_of_study":"","msr_release_tracker_id":"","msr_s2_match_type":"","msr_citation_count_updated":"","msr_published_date":"1982-07-01","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"","msr_journal_url":"","msr_s2_pdf_url":"","msr_year":0,"msr_citation_count":0,"msr_influential_citations":0,"msr_reference_count":0,"msr_s2_match_confidence":0,"msr_microsoftintellectualproperty":true,"msr_s2_open_access":false,"msr_s2_author_ids":[],"msr_pub_ids":[],"msr_hide_image_in_river":0,"footnotes":""},"msr-research-highlight":[],"research-area":[13561],"msr-publication-type":[193715],"msr-publisher":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-338456","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-algorithms","msr-locale-en_us"],"msr_publishername":"ACM","msr_edition":"ACM Transactions on Programming Languages and Systems","msr_affiliation":"","msr_published_date":"1982-07-01","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"455-495","msr_chapter":"","msr_isbn":"","msr_journal":"ACM Transactions on Programming Languages and Systems","msr_volume":"4","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"3","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":"460557","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","title":"proving-liveness-properties-of-concurrent-programs","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/Proving-Liveness-Properties-of-Concurrent-Programs.pdf","id":460557,"label_id":0}],"msr_related_uploader":"","msr_citation_count":0,"msr_citation_count_updated":"","msr_s2_paper_id":"","msr_influential_citations":0,"msr_reference_count":0,"msr_arxiv_id":"","msr_s2_author_ids":[],"msr_s2_open_access":false,"msr_s2_pdf_url":null,"msr_attachments":[],"msr-author-ordering":[{"type":"user_nicename","value":"Leslie Lamport","user_id":32614,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=Leslie Lamport"},{"type":"text","value":"Susan Owicki","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"article","related_content":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/338456","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\/338456\/revisions"}],"predecessor-version":[{"id":485289,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/338456\/revisions\/485289"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=338456"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=338456"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=338456"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=338456"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=338456"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=338456"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=338456"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=338456"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=338456"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=338456"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=338456"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=338456"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=338456"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}