University of Twente Student Theses


Runtime Permission Checking in Concurrent Java Programs

Gijsen, Stijn (2015) Runtime Permission Checking in Concurrent Java Programs.

[img] PDF
Abstract:The development of concurrent software is one of the key ways for software developers to benefit from the increasing number of processor cores found in computers and embedded devices. Developing concurrent programs is more difficult than developing sequential programs because of concurrency bugs such as data races, which occur when threads operate on one or more pieces of shared memory concurrently. Due to the non-deterministic order in which threads may be executed, these bugs are often hard to find. Permission specifications have been introduced to reason about shared memory in concurrent programs. These specifications make explicit which memory locations may be read from or written to by individual threads. A number of static verification solutions have been implemented for verifying programs against permission specifications, but no runtime checking solutions for permission specifications exist. In this master's thesis, we discuss ways to check permission specifications in a concurrent Java program at runtime. The specification language we use is that of VerCors, a static verification tool for permission specifications. We extend VerCors with a prototype for runtime checking that instruments Java source code with permission accounting and permission checks. We will also discuss various approaches for developing a production-ready runtime permission checker.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page