{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:28:02Z","timestamp":1774837682946,"version":"3.50.1"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61379039,61502442,61632005"],"award-info":[{"award-number":["61379039,61502442,61632005"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>Various progress properties have been proposed for concurrent objects, such as wait-freedom, lock-freedom, starvation-freedom and deadlock-freedom. However, none of them applies to concurrent objects with partial methods, i.e., methods that are supposed not to return under certain circumstances. A typical example is the lock_acquire method, which must not return when the lock has already been acquired.<\/jats:p>\n          <jats:p>In this paper we propose two new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF), for concurrent objects with partial methods. We also design four patterns to write abstract specifications for PSF or PDF objects under strongly or weakly fair scheduling, so that these objects contextually refine the abstract specifications. Our Abstraction Theorem shows the equivalence between PSF (or PDF) and the progress-aware contextual refinement. Finally, we generalize the program logic LiLi to have a new logic to verify the PSF (or PDF) property and linearizability of concurrent objects.<\/jats:p>","DOI":"10.1145\/3158108","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Progress of concurrent objects with partial methods"],"prefix":"10.1145","volume":"2","author":[{"given":"Hongjin","family":"Liang","sequence":"first","affiliation":[{"name":"Nanjing University, China \/ University of Science and Technology of China, China"}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[{"name":"Nanjing University, China \/ University of Science and Technology of China, China"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP","author":"Bostr\u00f6m Pontus","year":"2015","unstructured":"Pontus Bostr\u00f6m and Peter M\u00fcller . 2015 . Modular Verification of Finite Blocking in Non-terminating Programs . In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). 639\u2013663. Pontus Bostr\u00f6m and Peter M\u00fcller. 2015. Modular Verification of Finite Blocking in Non-terminating Programs. In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). 639\u2013663."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74061-2_15"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941487.1941509"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/3089528.3089536"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_19"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480886"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_36"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_19"},{"key":"e_1_2_2_9_1","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan (Newman) Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI 2016). 653\u2013669. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI 2016). 653\u2013669."},{"key":"e_1_2_2_10_1","unstructured":"Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann.  Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25873-2_22"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.18"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP","author":"Jacobs Bart","year":"2015","unstructured":"Bart Jacobs , Dragan Bosnacki , and Ruurd Kuiper . 2015 . Modular Termination Verification . In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). 664\u2013688. Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. 2015. Modular Termination Verification. In Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). 664\u2013688."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_24"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603123"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_17"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_13"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_25_1","volume-title":"System Programming: Coping with Parallelism. Technical Report RJ 5118","author":"Treiber R. Kent","year":"1986","unstructured":"R. Kent Treiber . 1986 . System Programming: Coping with Parallelism. Technical Report RJ 5118 . IBM Almaden Research Center . R. Kent Treiber. 1986. System Programming: Coping with Parallelism. Technical Report RJ 5118. IBM Almaden Research Center."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158108","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158108","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158108"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":25,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158108"],"URL":"https:\/\/doi.org\/10.1145\/3158108","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}