Modular verification of synchronization with reentrant locks

Download

index.pdf

Date

2010-07-28

Author

Bultan, Tevfik
Yu, Fang
Betin Can, Aysu

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

160
views

89
downloads

We present a modular approach for verification of synchronization behavior in concurrent programs that use reentrant locks. Our approach decouples the verification of the lock implementation from the verification of the threads that use the lock. This decoupling is achieved using lock interfaces that characterize the allowable execution order for the lock operations. We use a thread modular verification approach to check that each thread obeys the lock interface. We verify the lock implementation assuming that the threads behave according to the lock interface. We demonstrate that this approach can be used to verify synchronization behavior in Java programs that use reentrant lock implementations for synchronization.

Subject Keywords

Java, Synchronization, Semantics, Programming, Automation, USA Councils

URI

https://hdl.handle.net/11511/30144

DOI

https://doi.org/10.1109/memcod.2010.5558623

Collections

Graduate School of Informatics, Conference / Seminar

Suggestions

OpenMETU
Core

Standalone static binary executable rewriting for software protection Bican, Özgür Saygın; Şehitoğlu, Onur Tolga; Department of Computer Engineering (2015) This study introduces a static binary rewriting method for improving security of executable binaries. For software security, when the network and host-based precautions are passed by the adversary or they are not present at all, the software has to defend itself. Nevertheless, applying software protection methods during software development requires extra source code development and know-how. Furthermore, these methods inherently make the software undesirably complex. Applying these methods after compilatio...
Some Studies on CCZ-Equivalence of the Inverse Function Fidan, Mehtap; ÖZBUDAK, Ferruh; Department of Cryptography (2021-9-28) Most cryptographic systems, like block ciphers, depend heavily on vectorial Boolean functions. A function with good cryptological properties should have low differential uniformity which is invariant under some equivalence classes. The more general one of these is CCZ-equivalence which is introduced by Carlet, Charpin and Zinoviev in 1998. In cryptography, CCZ-equivalence gained an interest since it preserves many significant properties like differential uniformity. Looking for permutations within the CCZ-c...
Automatic Detection of Shared Objects in Multithreaded Java Programs Tolubaeva, Munara; Betin Can, Aysu (2008-12-12) This paper presents a simple and efficient automated tool called DoSSO that detects shared objects in multithreaded Java programs. Our main goal is to help programmers see all potentially shared objects that may cause some complications at runtime. This way programmers can implement a concurrent software without considering synchronization issues and then use appropriate locking mechanism based on the DoSSO results. To illustrate the effectiveness of our tool, we have petformed an experiment on a multithrea...
Nonblocking hierarchical control of decentralized des Schmidt, Klaus Verner; Moor, Thomas (null; 2005-12-01) This work considers a hierarchical control architecture for a class of discrete event systems which can also be applied to decentralized control systems. It is shown that nonblocking supervisory control on the high level of the hierarchy results in nonblocking and hierarchically consistent control on the low level. Copyright © 2005 IFAC.
Concurrency control in distributed databases through dummy locks Halıcı, Uğur (1990-10-01) An optimistic scheme, called ODL, that uses dummy locks to test the validity of a transaction for concurrency control in distributed database systems is suggested. The dummy locks are long-term locks; however, they do not conflict with any other lock. By the use of long-term dummy locks, the need for the information about the write sets of validated transactions is eliminated, and during the validation test only the related sites are checked. Also, the transactions to be aborted are immediately recognized b...

Citation Formats

T. Bultan, F. Yu, and A. Betin Can, “Modular verification of synchronization with reentrant locks,” 2010, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/30144.