Automated Commonsense Reasoning Techniques for Concurrent Data Structure Synthesis




Journal Title

Journal ISSN

Volume Title



Multiprocessors are ubiquitous in today’s computing devices ranging from smartphones, IoT micro-controllers, personal laptops to servers in data centers. Programming multiprocessors is a non-trivial task and is largely practised as an art. Due to limits imposed by Moore’s law on the computing power of microprocessors, writing software that runs on multiple processors is an increasing need. Programs written to run on multiple processors are termed concurrent programs as they contain concurrent threads of program execution over memory that is shared. The area of concurrent data structures focuses on developing data structures that can store information correctly when multiple threads try to access and modify the data structure concurrently. The transition from data structures that are designed to work with a single thread of execution to a concurrent version is non-trivial. There are several possible ways in which threads can interfere that can result in incorrect information being stored in the data structure. Furthermore, concurrent programs are notoriously hard to design and debug, even when the number of lines in the code is small. At the same time, human experts cleverly reason about all possible concurrent interactions of sequential code and arrive at correct concurrent algorithms. This thesis captures the techniques used by a human expert when designing concurrent data structures and makes that expert knowledge executable on a computer. Thus, the tool that we have developed named Locksynth automatically generates correct concurrent data structure code in a manner similar to how a human would approach the problem. The generated code is guaranteed to be correct by construction. Automatically generating code that is correct by construction is an important problem in computing due to the sheer complexity of software systems being developed today. This thesis, thus, makes research contributions to the area of automated concurrent data structure synthesis.



Computer Science