Transformational Specification of Out-of-Thin-Air Memory Models

Much of the performance in today’s computing devices such as mobiles, desktops, supercomputers, etc. can be attributed to concurrency – the ability to perform more than one task simultaneously. In addition, performance of software that run on such devices greatly benefit from the compiler (software that translates our code to be run by hardware) that optimizes them. Interplay between compiler optimizations and such concurrent devices have been known to cause erroneous software behaviors, which can been fatal. The goal of this project is to explain these concurrent behaviors precisely in terms of the optimizations that are done by the compiler. We will utilize this information to synthesize a concurrent model which can help us rule out optimizations that can cause software behave erroneously. We will use such a model to develop reasoning techniques which will help in testing and verifying pieces of critical software.

Faculty Supervisor:

Clark Verbrugge

Student:

Partner:

University of Kent

Discipline:

Computer science

Sector:

Education

University:

McGill University

Program: