{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T14:52:37Z","timestamp":1774795957238,"version":"3.50.1"},"reference-count":54,"publisher":"Emerald","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,5,18]]},"abstract":"<jats:p>Implementations of concurrent objects should guarantee linearizability and a progress property such as wait-freedom, lock-freedom, starvation-freedom, or deadlock-freedom. These progress properties describe conditions under which a method call is guaranteed to complete. However, they fail to describe how clients are affected, making it difficult to utilize them in layered and modular program verification. Also we lack verification techniques for starvation-free or deadlock-free objects. They are challenging to verify because the fairness assumption introduces complicated interdependencies among progress of threads. Even worse, none of the existing results 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 tutorial we examine the progress properties of concurrent objects. We formulate each progress property (together with linearizability as a basic correctness requirement) in terms of contextual refinement. This essentially gives us progress-aware abstraction for concurrent objects. Thus, when verifying clients of the objects, we can soundly replace the concrete object implementations with their abstractions, achieving modular verification. For concurrent objects with partial methods, we formulate two new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF). We also design four patterns to write abstractions for PSF or PDF objects under strongly or weakly fair scheduling, so that these objects contextually refine their abstractions. Finally, we introduce a rely-guarantee style program logic LiLi for verifying linearizability and progress together for concurrent objects. It unifies thread-modular reasoning about all the six progress properties (wait-freedom, lock-freedom, starvation-freedom, deadlock-freedom, PSF and PDF) in one framework. We have successfully applied LiLi to verify starvation-freedom or deadlock-freedom of representative algorithms such as lock-coupling lists, optimistic lists and lazy lists, and PSF or PDF of lock algorithms.<\/jats:p>","DOI":"10.1561\/2500000041","type":"journal-article","created":{"date-parts":[[2020,5,18]],"date-time":"2020-05-18T08:50:47Z","timestamp":1589791847000},"page":"282-414","source":"Crossref","is-referenced-by-count":2,"title":["Progress of Concurrent Objects"],"prefix":"10.1561","volume":"5","author":[{"given":"Hongjin","family":"Liang","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University ,","place":["China"]}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University ,","place":["China"]}]}],"member":"140","published-online":{"date-parts":[[2020,5,18]]},"reference":[{"issue":"3","key":"2026032910224381900_ref001","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/203095.201069","article-title":"Conjoining specifications","volume":"17","author":"Abadi","year":"1995","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032910224381900_ref002","first-page":"340","article-title":"Wait-free data structures in the asynchronous PRAM model","volume-title":"SPAA","author":"Aspnes","year":"1990"},{"issue":"2","key":"2026032910224381900_ref003","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/s002360050116","article-title":"Refinement of fair action systems","volume":"35","author":"Back","year":"1998","journal-title":"Acta Inf"},{"key":"2026032910224381900_ref004","first-page":"639","volume-title":"Modular verification of finite blocking in non-terminating programs","author":"Bostr\u00f6m","year":"2015"},{"key":"2026032910224381900_ref005","first-page":"211","article-title":"Ownership types for safe programming: Preventing data races and deadlocks","volume-title":"OOPSLA","author":"Boyapati","year":"2002"},{"key":"2026032910224381900_ref006","first-page":"233","volume-title":"Modular safety checking for fine-grained concurrency","author":"Calcagno","year":"2007"},{"issue":"5","key":"2026032910224381900_ref007","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/1941487.1941509","article-title":"Proving program termination","volume":"54","author":"Cook","year":"2011","journal-title":"Commun. ACM"},{"key":"2026032910224381900_ref008","first-page":"176","volume-title":"Modular termination verification for non-blocking concurrency","author":"da Rocha Pinto","year":"2016"},{"issue":"1","key":"2026032910224381900_ref009","doi-asserted-by":"crossref","first-page":"4:1","DOI":"10.1145\/1889997.1890001","article-title":"Mechanically verified proof obligations for linearizability","volume":"33","author":"Derrick","year":"2011","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032910224381900_ref010","first-page":"97","article-title":"Formal verification of a practical lock-free queue algorithm","volume-title":"FORTE","author":"Doherty","year":"2004"},{"key":"2026032910224381900_ref011","first-page":"284","article-title":"Formalising progress properties of non-blocking programs","volume-title":"ICFEM","author":"Dongol","year":"2006"},{"key":"2026032910224381900_ref012","volume-title":"TaDA live: Compositional reasoning for termination of fine-grained concurrent programs","author":"D\u2018Osualdo","year":"2019"},{"key":"2026032910224381900_ref013","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1145\/1480881.1480922","article-title":"Local rely-guarantee reasoning","volume-title":"POPL","author":"Feng","year":"2009"},{"key":"2026032910224381900_ref014","first-page":"252","volume-title":"Abstraction for concurrent objects","author":"Filipovi\u0107","year":"2009"},{"key":"2026032910224381900_ref015","first-page":"287","article-title":"Intensional and ex-tensional characterisation of global progress in the calculus","volume-title":"CONCUR","author":"Fossati","year":"2012"},{"key":"2026032910224381900_ref016","first-page":"16","volume-title":"Proving that non-blocking algorithms don\u2019t block","author":"Gotsman","year":"2009"},{"key":"2026032910224381900_ref017","first-page":"453","volume-title":"Liveness-preserving atomicity abstraction","author":"Gotsman","year":"2011"},{"key":"2026032910224381900_ref018","first-page":"256","volume-title":"Linearizability with ownership transfer","author":"Gotsman","year":"2012"},{"key":"2026032910224381900_ref019","first-page":"653","volume-title":"CertiKOS: An extensible architecture for building certified concurrent OS kernels","author":"Gu","year":"2016"},{"key":"2026032910224381900_ref020","first-page":"300","article-title":"A pragmatic implementation of non-blocking linked-lists","volume-title":"DISC","author":"Harris","year":"2001"},{"key":"2026032910224381900_ref021","first-page":"3","article-title":"A lazy concurrent list-based set algorithm","volume-title":"OPODIS","author":"Heller","year":"2005"},{"key":"2026032910224381900_ref022","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1145\/1007912.1007944","article-title":"A scalable lock-free stack algorithm","volume-title":"SPAA","author":"Hendler","year":"2004"},{"issue":"1","key":"2026032910224381900_ref023","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1006\/inco.2001.3085","article-title":"Fair simulation","volume":"173","author":"Henzinger","year":"2002","journal-title":"Inf. Comput"},{"key":"2026032910224381900_ref024","volume-title":"The Art of Multiprocessor Programming","author":"Herlihy","year":"2008"},{"key":"2026032910224381900_ref025","first-page":"313","volume-title":"On the nature of progress","author":"Herlihy","year":"2011"},{"issue":"3","key":"2026032910224381900_ref026","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","article-title":"Linearizability: A correctness condition for concurrent objects","volume":"12","author":"Herlihy","year":"1990","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032910224381900_ref027","first-page":"124","volume-title":"Quantitative reasoning for proving lock-freedom","author":"Hoffmann","year":"2013"},{"key":"2026032910224381900_ref028","first-page":"664","volume-title":"Modular termination verification","author":"Jacobs","year":"2015"},{"issue":"4","key":"2026032910224381900_ref029","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","article-title":"Tentative steps toward a development method for interfering programs","volume":"5","author":"Jones","year":"1983","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032910224381900_ref030","first-page":"637","volume-title":"Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning","author":"Jung","year":"2015"},{"key":"2026032910224381900_ref031","first-page":"639","volume-title":"Proving linearizability using partial orders","author":"Khyzha","year":"2017"},{"key":"2026032910224381900_ref032","first-page":"378","article-title":"A basis for verifying multithreaded programs","volume-title":"ESOP","author":"Leino","year":"2009"},{"key":"2026032910224381900_ref033","first-page":"407","article-title":"Deadlock-free channels and locks","volume-title":"ESOP","author":"Leino","year":"2010"},{"key":"2026032910224381900_ref034","first-page":"459","volume-title":"Modular verification of linearizability with non-fixed linearization points","author":"Liang","year":"2013"},{"key":"2026032910224381900_ref035","first-page":"385","volume-title":"A program logic for concurrent objects under fair scheduling","author":"Liang","year":"2016"},{"key":"2026032910224381900_ref036","doi-asserted-by":"crossref","DOI":"10.1145\/3158108","volume-title":"Progress of concurrent objects with partial methods","author":"Liang","year":"2018"},{"key":"2026032910224381900_ref037","unstructured":"Liang, H. and X.Feng (2018b). \u201cProgress of concurrent objects with partial methods (extended version)\u201d. In: Tech. Rep. https:\/\/cs.nju.edu.cn\/hongjin\/papers\/popl18-partial-tr.pdf."},{"key":"2026032910224381900_ref038","doi-asserted-by":"crossref","DOI":"10.1145\/2603088.2603123","volume-title":"Compositional verification of termination-preserving refinement of concurrent programs","author":"Liang","year":"2014"},{"key":"2026032910224381900_ref039","first-page":"227","volume-title":"Characterizing progress properties of concurrent objects via contextual refinements","author":"Liang","year":"2013"},{"issue":"1","key":"2026032910224381900_ref040","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/103727.103729","article-title":"Algorithms for scalable synchronization on shared-memory multiprocessors","volume":"9","author":"Mellor-Crummey","year":"1991","journal-title":"ACM Trans. Comput. Syst"},{"key":"2026032910224381900_ref041","first-page":"73","article-title":"High performance dynamic lock-free hash tables and list-based sets","volume-title":"SPAA","author":"Michael","year":"2002"},{"key":"2026032910224381900_ref042","first-page":"267","article-title":"Simple, fast, and practical non-blocking and blocking concurrent queue algorithms","volume-title":"PODC","author":"Michael","year":"1996"},{"key":"2026032910224381900_ref043","first-page":"137","article-title":"Variables as resource in Hoare logics","volume-title":"LICS","author":"Parkinson","year":"2006"},{"key":"2026032910224381900_ref044","first-page":"144","article-title":"Progress guarantee for parallel programs via bounded lock-freedom","volume-title":"PLDI","author":"Petrank","year":"2009"},{"key":"2026032910224381900_ref045","first-page":"193","volume-title":"Towards a thread-local proof technique for starvation freedom","author":"Schellhorn","year":"2016"},{"key":"2026032910224381900_ref046","first-page":"369","article-title":"A proof technique for rely\/guarantee properties","volume-title":"FSTTCS","author":"Stark","year":"1985"},{"key":"2026032910224381900_ref047","first-page":"479","article-title":"Shared-state design modulo weak and strong process fairness","volume-title":"FORTE","author":"St\u00f8len","year":"1992"},{"key":"2026032910224381900_ref048","first-page":"909","volume-title":"A higher-order logic for concurrent termination-preserving refinement","author":"Tassarotti","year":"2017"},{"key":"2026032910224381900_ref049","volume-title":"Tech. Rep","author":"Treiber","year":"1986"},{"key":"2026032910224381900_ref050","first-page":"377","article-title":"Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency","volume-title":"ICFP","author":"Turon","year":"2013"},{"key":"2026032910224381900_ref051","first-page":"343","volume-title":"Logical relations for fine-grained concurrency","author":"Turon","year":"2013"},{"key":"2026032910224381900_ref052","article-title":"Modular fine-grained concurrency verification","volume-title":"Tech. Rep","author":"Vafeiadis","year":"2008"},{"key":"2026032910224381900_ref053","first-page":"602","article-title":"Static deadlock detection for java libraries","volume-title":"ECOOP","author":"Williams","year":"2005"},{"issue":"2","key":"2026032910224381900_ref054","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF01211617","article-title":"The rely-guarantee method for verifying shared variable concurrent programs","volume":"9","author":"Xu","year":"1997","journal-title":"Formal Asp. Comput"}],"container-title":["Foundations and Trends\u00ae in Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/5\/4\/282\/11044206\/2500000041en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/5\/4\/282\/11044206\/2500000041en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T14:22:52Z","timestamp":1774794172000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftpgl\/article\/5\/4\/282\/1328327\/Progress-of-Concurrent-Objects"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,18]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,5,18]]}},"URL":"https:\/\/doi.org\/10.1561\/2500000041","relation":{},"ISSN":["2325-1107","2325-1131"],"issn-type":[{"value":"2325-1107","type":"print"},{"value":"2325-1131","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,5,18]]}}}