Côd QR

Formal Modeling and Verification of Lycklama and Hadzilacos’s Mutual Exclusion Algorithm

This study describes our thorough experience of formal modeling and exhaustive verification of concurrent systems, particularly mutual exclusion algorithms. The experience focuses on Lycklama and Hadzilacos’s (LH) mutual exclusion algorithm. LH rests on the reduced size of the shared state, contains...

Disgrifiad llawn

Wedi'i Gadw mewn:
Prif Awdur: Libero Nigro
Fformat: Artigo
Iaith:Inglês
Cyhoeddwyd: MDPI AG 2024-08-01
Cyfres:Mathematics
Pynciau:
concurrency/parallelism
mutual exclusion algorithms
properties
atomic and non-atomic memory models
formal modelling
exhaustive model checking
Mynediad Ar-lein:https://www.mdpi.com/2227-7390/12/16/2443
Tagiau: Ychwanegu Tag
Dim Tagiau, Byddwch y cyntaf i dagio'r cofnod hwn!

Eitemau Tebyg