Diogo Sousa (2013)

MSc Student

in

MSc dissertation: Preventing Atomicity Violations with Contracts  
Co-adviser: Prof. Carla Ferreira
Period: September 2012 — September 2013
Grade: 19/20 points
Papers in Journals: ComSIS 8(2) 2011 (DOI).
Papers in International Conferences and Workshops: PADTAD'12 (DOI), PADTAD 2010 (DOI), PADTAD 2009 (DOI)
Papers in national conferences: INForum'13, INForum'12 (link), INForum'10 (link)
Work context: Synergy-VM project (funded by the National Science Foundation, PI: Prof. João Lourenço)

Diogo Sousa is currently working in his MSc thesis entitled "Preventing Atomicity Violations with Contracts".  Additionally, he is adapting MoTH, our static analysis tool for detecting of high-level data races, to use a Single Static Assignment internal data representation and then will inroduce points-to and happens-before analysis to the tool.

Diogo is working with me since he was a bachelor student (November 2008). He has undertake multiple small tasks and also conducted some research of his own related to the Detection of Anomalies in Transactional Memory Programs.

MSc thesis abstract (draft):

Concurrent programming is a difficult and error-prone task because the programmer must reason about the multiple threads of execution and their possible interleavings. A concurrent program must synchronize the concurrent accesses to shared memory regions, but this is not enough to prevent all anomalies that can arise in a concurrent setting. The programmer can misidentify the scope of the regions of code that need to be atomic, resulting in atomicity violations and failing to ensure the correct behavior of the program. Executing a sequence of atomic operations may lead to incorrect results when these operations are co-related. In this case, the programmer may be required to enforce the sequential execution of those operations as a whole to avoid atomicity violations. This situation is specially common when the developer makes use of services from third-party packages or modules.

This thesis proposes a methodology, based on the design by contract methodology, to specify which sequences of operations must be executed atomically. We developed an analysis that statically verifies that a client of a module is respecting its contract, allowing the programmer to identify the source of possible atomicity violations.