The development of concurrent software is one of the key ways for software de- velopers to benefit from the increasing number of processor cores found in com- puters and embedded devices. Through multithreading, multiple processors can be used to speed up computations or to improve user experiences.

Developing concurrent programs is more difficult than developing sequential pro- grams because of concurrency bugs such as thread interference and data races, which occur when threads operate on one or more pieces of shared memory con- currently. Due to the non-deterministic order in which multiple threads may be executed, these bugs are often hard to find.

Permission specifications have been introduced to reason about shared memory in concurrent programs. By introducing a concept of permissions, these specific- ations make explicit which memory locations may be read from or written to by individual threads. A number of static verification solutions have been imple- mented for verifying programs against permission specifications, but no runtime checking solutions for permission specifications exist, despite the fact that concur- rency is also often used in software that is not easily checked statically, such as user interfaces.

In this master’s thesis, we will discuss ways to track and check permission specific- ations in a concurrent Java program at runtime. The specification language we use is the annotation language 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.