Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. EPFL thesis
  4. Safety, Liveness and Parallelism in Concurrent Computing
 
doctoral thesis

Safety, Liveness and Parallelism in Concurrent Computing

Bushkov, Victor  
2015

The correctness of a shared object, which can be accessed by several processes concurrently, is specified through two different kinds of properties - safety and liveness. When implementing a shared object it is important to specify its correctness in a such way that it should be feasible under given assumptions. In this work we study the question of implementability of shared objects that satisfy certain safety and liveness properties under certain assumptions. In particular, we study implementability of liveness properties of transactional memory (TM) shared objects with strict serializability, a strong safety property. TM allows a programmer to encapsulate pieces of sequential code within transactions that run concurrently and it ensures that transactions run in some consistent manner by committing or aborting them. First, we give a formal definition of a liveness property in the TM context. Then, we proceed to show that certain classes of liveness properties of TM can not be implemented with strict serializability in a system in which processes are prone to failures. We also show that, in general, we cannot find a weakest non-implementable (resp. strongest implementable) liveness of TM when we require some common safety property like strict serializability. Moreover, we generalize this result to other shared object types and give a characterization of safety properties for which we can find weakest non-implementable (resp. strongest implementable) liveness. In addition to correctness properties we study the limitations of parallelism which affects performance and scalability of implementations. Specifically, we show that we cannot implement a TM which guarantees disjoint-access parallelism, which say that transactions do not need to synchronize unless they access the same application objects, while guaranteeing very weak safety and the weakest non-blocking liveness.

  • Files
  • Details
  • Metrics
Type
doctoral thesis
DOI
10.5075/epfl-thesis-6758
Author(s)
Bushkov, Victor  
Advisors
Guerraoui, Rachid  
Jury

Prof. Michael Christoph Gastpar (président) ; Prof. Rachid Guerraoui (directeur de thèse) ; Prof. Viktor Kuncak, Prof. Petr Kuznetsov, Prof. Pascal Felber (rapporteurs)

Date Issued

2015

Publisher

EPFL

Publisher place

Lausanne

Public defense year

2015-12-09

Thesis number

6758

Total of pages

139

Subjects

concurrent algorithms

•

shared memory

•

transactional memory

Note

La page de titre du PDF mentionne par erreur comme président du jury M. Odersky au lieu de M.C. Gastpar

EPFL units
DCL  
Faculty
IC  
School
IIF  
Doctoral School
EDIC  
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/121652
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés