Zobrazeno 1 - 10
of 71
pro vyhledávání: '"Lamport's bakery algorithm"'
Autor:
Rob Sumners
Publikováno v:
Electronic Proceedings in Theoretical Computer Science. 327:47-60
A common technique for checking properties of complex state machines is to build a finite abstraction then check the property on the abstract system -- where a passing check on the abstract system is only transferred to the original system if the abs
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9c85dab65489699a25ba407330b750ca
https://doi.org/10.4204/eptcs.327.4
https://doi.org/10.4204/eptcs.327.4
Autor:
Yoram Moses, Katia Patkin
Publikováno v:
Theoretical Computer Science. 751:46-60
A new approach to the study and analysis of Mutual Exclusion (ME) algorithms is presented, based on identifying the priority relation that the ME algorithm constructs. It is argued that by analyzing how a process detects that it has priority over all
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::cf6bfa4eb9b55d296164c90490b149f6
https://doi.org/10.1016/j.tcs.2016.12.015
https://doi.org/10.1016/j.tcs.2016.12.015
Autor:
Rob Sumners
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 249, Iss Proc. ACL2Workshop 2017, Pp 78-94 (2017)
We present a series of definitions and theorems demonstrating how to reduce the requirements for proving system refinements ensuring containment of fair stuttering runs. A primary result of the work is the ability to reduce the requisite proofs on ru
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::42350a711b21dc2647ac805f9a1ce040
https://doi.org/10.4204/eptcs.249.6
https://doi.org/10.4204/eptcs.249.6
Autor:
Amirhossein Sayyadabdi, Mohsen Sharifi
Publikováno v:
ICPP Workshops
Computer systems are designed to make resources available to users and users may be interested in some resources more than others, therefore, a coordination scheme is required to satisfy the users' requirements. This scheme may implement certain poli
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::88e125669609738630b452f81bc94a94
Autor:
Leslie Lamport
Publikováno v:
Concurrency: the Works of Leslie Lamport
This paper describes the bakery algorithm for implementing mutual exclusion. I have invented many concurrent algorithms. I feel that I did not invent the bakery algorithm, I discovered it. Like all shared-memory synchronization algorithms, the bakery
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::bbccb78bccd2ee423ba4ca960ec77c54
https://doi.org/10.1145/3335772.3335782
https://doi.org/10.1145/3335772.3335782
Autor:
Hagit Attiya, Jennifer L. Welch
Publikováno v:
Concurrency: the Works of Leslie Lamport
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f8f52e49c02b0d89b7d6ad933e8b2b55
https://doi.org/10.1145/3335772.3335776
https://doi.org/10.1145/3335772.3335776
Publikováno v:
IEEE Access, Vol 5, Pp 20866-20879 (2017)
In the Internet of Things scene, the wireless sensor network (WSN) is widely used to monitor and perceive various context environments. The efficient utilization of time division multiple access (TDMA) slot resource has attracted more and more attent
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::dab2068bb727d6f57dfaa0ee3c4ebd61
https://doi.org/10.1109/access.2017.2758340
https://doi.org/10.1109/access.2017.2758340
Publikováno v:
SIGMOD Conference
Lock managers are a crucial component of modern distributed systems. However, with the increasing availability of fast RDMA-enabled networks, traditional lock managers can no longer keep up with the latency and throughput requirements of modern syste
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a0d5445c5680ff07d07994e254a9725b
https://doi.org/10.1145/3183713.3196890
https://doi.org/10.1145/3183713.3196890
Publikováno v:
2017 9th International Conference on Intelligent Human-Machine Systems and Cybernetics (IHMSC).
In this article, Black White (BW) Bakery algorithm is formally analyzed and verified in SPIN model checker. BW Bakery algorithm is first modeled in PROMELA and the model is then verified in SPIN. Mutual exclusion property for the BW Bakery model is v
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ca895b966382dab2a5d5287eb3e736d8
https://doi.org/10.1109/ihmsc.2017.203
https://doi.org/10.1109/ihmsc.2017.203
Autor:
Wim H. Hesselink
Publikováno v:
Science of computer programming, 78(9), 1622-1638. ELSEVIER SCIENCE BV
Proof assistants like PVS can be used fruitfully for the design and verification of concurrent algorithms. The technique is presented here by applying it to Lamport's Bakery algorithm. The proofs for safety properties such as mutual exclusion, first-
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6d42babd28751e46856ef9c9af8dd53f
https://doi.org/10.1016/j.scico.2013.03.003
https://doi.org/10.1016/j.scico.2013.03.003