Show/Hide Menu
Hide/Show Apps
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Open Science Policy
Open Science Policy
Open Access Guideline
Open Access Guideline
Postgraduate Thesis Guideline
Postgraduate Thesis Guideline
Communities & Collections
Communities & Collections
Help
Help
Frequently Asked Questions
Frequently Asked Questions
Guides
Guides
Thesis submission
Thesis submission
MS without thesis term project submission
MS without thesis term project submission
Publication submission with DOI
Publication submission with DOI
Publication submission
Publication submission
Supporting Information
Supporting Information
General Information
General Information
Copyright, Embargo and License
Copyright, Embargo and License
Contact us
Contact us
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
149
views
82
downloads
Cite This
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
IEEE
ACM
APA
CHICAGO
MLA
BibTeX
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.