Interface-based specification and verification of concurrency controllers

Bultan, Tevfik
Betin Can, Aysu
We present a modular approach to specification and verification of concurrency controllers by decoupling their behavior and interface specifications. The behavior specification of a concurrency controller defines how its shared variables change their values whereas the interface specification defines the order in which a client thread should call its methods. We show that the concurrency controllers can be designed modularly by composing their interfaces. We separate the verification of the concurrency controllers from the verification of the threads that use them. For the verification of the concurrency controllers we use infinite state verification techniques which enable us to verify controllers with parameterized constants and arbitrary number of user threads. We automatically generate Java monitors from the concurrency controller specifications which preserve the verified properties. For the thread verification we use finite state program verification tools which enable us to verify Java threads without any restrictions. We show that the user threads can be verified using stubs generated from the concurrency controller interfaces which improves the efficiency of the thread verification significantly.
Electronic Notes in Theoretical Computer Science


Linear static analysis of large structural models on pc clusters
Özmen, Semih; Toker, Kurç; Department of Civil Engineering (2009)
This research focuses on implementing and improving a parallel solution framework for the linear static analysis of large structural models on PC clusters. The framework consists of two separate programs where the first one is responsible from preparing data for the parallel solution that involves partitioning, workload balancing, and equation numbering. The second program is a fully parallel nite element program that utilizes substructure based solution approach with direct solvers. The first step of data...
Cortex-M4 optimizations for {R, M} LWE schemes
Alkım, Erdem; Bilgin, Yusuf Alper; Cenk, Murat; Gérard, François (2020-06-01)
This paper proposes various optimizations for lattice-based key encapsulation mechanisms (KEM) using the Number Theoretic Transform (NTT) on the popular ARM Cortex-M4 microcontroller. Improvements come in the form of a faster code using more efficient modular reductions, optimized small-degree polynomial multiplications, and more aggressive layer merging in the NTT, but also in the form of reduced stack usage. We test our optimizations in software implementations of Kyber and NewHope, both round 2 candidate...
Performance Evaluation of Different Real-Time Motion Controller Topologies Implemented on a FPGA
MUTLU, B. R.; Yaman, Ulaş; Dölen, Melik; Koku, Ahmet Buğra (2009-11-18)
This paper presents a comprehensive comparison of several real-time motion controller topologies implemented on a field programmable gate array (FPGA). Controller topologies are selected as proportional-integral-derivative controller with command feedforward, sliding mode controller, fuzzy controller, and a hysteresis controller. Controllers and other necessary modules are developed using Verilog HDL and they are implemented on a ML505 development board with a Xilinx Virtex-5 FPGA chip. In order to take ful...
Modular verification of synchronization with reentrant locks
Bultan, Tevfik; Yu, Fang; Betin Can, Aysu (2010-07-28)
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 t...
Scalable computational steering system for vizualization of large scale CFD simulations
Tonkal, Ozan Çağrı; Pehlivan, Sercan; Sezer Uzol, Nilay; İşler, Veysi (2002-06-27)
A general-purpose computational steering system (POSSE) which can be coupled to any C/C++ simulation code, has been developed and tested with a 3-D Navier-Stokes flow solver (PUMA2). This paper illustrates how to use “computational steering” with PUMA2 to visualize CFD solutions while they are being computed, and even change the input data while it is running. In addition, the visualizations can be displayed using virtual reality facilities (such as CAVEs and RAVEs) to better understand the 3-D nature of th...
Citation Formats
T. Bultan and A. Betin Can, “Interface-based specification and verification of concurrency controllers,” Electronic Notes in Theoretical Computer Science, pp. 464–479, 2003, Accessed: 00, 2020. [Online]. Available: