Starvation-free mutual exclusion with semaphores

DOI10.1007/s00165-011-0219-yzbMath1298.68192OpenAlexW2035587272MaRDI QIDQ469360

Wim H. Hesselink, Mark IJbema

Publication date: 10 November 2014

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-011-0219-y

zbMATH Keywords

refinementmutual exclusionbinary semaphoresemaphorestarvation freedom

Mathematics Subject Classification ID

Nonnumerical algorithms (68W05) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Starvation-free mutual exclusion with semaphores

Uses Software

• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Starvation-free mutual exclusion with semaphores
• The existence of refinement mappings
• Verification of sequential and concurrent programs
• Fair mutual exclusion with unfair P and V operations
• An axiomatic proof technique for parallel programs
• A starvation-free solution to the mutual exclusion problem
• Forward and backward simulations. I. Untimed Systems
• Universal extensions to simulate specifications
• Splitting forward simulations to cope with liveness
• Monitors
• A new solution of Dijkstra's concurrent programming problem
• Completeness of ASM Refinement
• The structure of the “THE”-multiprogramming system