Verifiable concurrent programming using concurrency controllers

Date

2004-09-24

Author

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

198
views

0
downloads

We present a framework for verifiable concurrent programming in Java based on a design pattern for concurrency controllers. Using this pattern, a programmer can write concurrency controller classes defining a synchronization policy by specifying a set of guarded commands and without using any of the error-prone synchronization primitives of Java. We present a modular verification approach that exploits the modularity of the proposed pattern, i.e., decoupling of the controller behavior from the threads that use the controller To verify the controller behavior (behavior verification) we use symbolic and infinite state model checking techniques, which enable verification of controllers with parameterized constants, unbounded variables and arbitrary number of user threads. To verify that the threads use a controller in the specified manner (interface verification) we use explicit state model checking techniques, which allow verification of arbitrary thread implementations without any restrictions. We show that the correctness of the user threads can be verified using the concurrency controller interfaces as stubs, which improves the efficiency of the interface verification significantly. We also show that the concurrency controllers can be automatically optimized using the specific notification pattern. We demonstrate the effectiveness of our approach on a Concurrent Editor implementation which consists of 2800 lines of Java code with remote procedure calls and complex synchronization constraints.

Subject Keywords

Concurrent computing , Yarn , Computer science , Programming profession , Java , Condition monitoring , Error correction , Concurrency control , Safety

URI

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

DOI

https://doi.org/10.1109/ase.2004.1342742

Collections

Graduate School of Informatics, Conference / Seminar

Suggestions

OpenMETU
Core

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...
Verifiable web services with hierarchical interfaces Betin Can, Aysu (2005-07-15) We propose an Hierarchical State Machine (HSM) model for specifying behavioral interfaces of peers participating in a composite web service. We integrate the HSM model to a design pattern which is supported by a modular verification technique that can 1) statically analyze the properties about global interactions of a composite web service and 2) check the conformance of the Java implementations of the participant peers to their interfaces. We extend the synchronizability analysis to HSMs to efficiently ide...
Implementation of concurrent constraint transaction logic and its user interface Altunyuva, Fethi; Karagöz, Pınar; Department of Computer Engineering (2006) This thesis implements a logical formalism framework called Concurrent Constraint Transaction Logic (abbr.,CCTR) which was defined for modeling and scheduling of workflows under resource allocation and cost constraints and develops an extensible and flexible graphical user interface for the framework. CCTR extends Concurrent Transaction Logic and integrates with Constraint Logic Programming to find the correct scheduling of tasks that involves resource and cost constraints. The developed system, which integ...
Concurrency control in distributed databases through time intervals and short-term locks Halıcı, Uğur (Institute of Electrical and Electronics Engineers (IEEE), 1989) A method for concurrency control in distributed database management systems that increases the level of concurrent execution of transactions, called ordering by serialization numbers (OSN), is proposed. The OSN method works in the certifier model and uses time-interval techniques in conjunction with short-term locks to provide serializability and prevent deadlocks. The scheduler is distributed, and the standard transaction execution policy is assumed, that is, the read and write operations are issued contin...
Content based packet filtering in linux kernel using deterministic finite automata Bilal, Tahir; Şehitoğlu, Onur Tolga; Department of Computer Engineering (2011) In this thesis, we present a content based packet filtering Architecture in Linux using Deterministic Finite Automata and iptables framework. New generation firewalls and intrusion detection systems not only filter or inspect network packets according to their header fields but also take into account the content of payload. These systems use a set of signatures in the form of regular expressions or plain strings to scan network packets. This scanning phase is a CPU intensive task which may degrade network p...

Citation Formats

A. Betin Can, “Verifiable concurrent programming using concurrency controllers,” 2004, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/30977.