Formalising progress properties of non-blocking programs
Contribuinte(s) |
Z. Liu J. He |
---|---|
Data(s) |
01/01/2006
|
Resumo |
A non-blocking program is one that uses non-blocking primitives, such as load-linked/store-conditional and compare-and-swap, for synchronisation instead of locks so that no process is ever blocked. According to their progress properties, non-blocking programs may be classified as wait-free, lock-free or obstruction-free. However, a precise description of these properties does not exist and it is not unusual to find a definition that is ambiguous or even incorrect. We present a formal definition of the progress properties so that any confusion is removed. The formalisation also allows one to prove the widely believed presumption that wait-freedom is a special case of lock-freedom, which in turn is a special case of obstruction-freedom. |
Identificador | |
Idioma(s) |
eng |
Publicador |
Springer-Verlag |
Palavras-Chave | #E1 #280302 Software Engineering #780000 - Non-Oriented Research #280301 Programming Techniques #280303 Programming Languages #280402 Mathematical Logic and Formal Languages #280403 Logics and Meanings of Programs |
Tipo |
Conference Paper |