Time Partitioning in Goblint: Extending region analysis with happens-before information
Name
Vootele Rõtov
Abstract
The concurrent nature of device drivers makes them notoriously
difficult to manually debug. Goblint, a static analysis framework tries to
automatically verify the inexistence of data races. The key challenge in doing
that is the precision of the analysis. This paper proposes an enhancement to the region analysis of Goblint to incorporate domain-specific happens-before
guarantees. The proposed addition is implemented and evaluated on the Goblint benchmark suite. We show that the given enhancement increases the precision of Goblint when analysing character drivers.
difficult to manually debug. Goblint, a static analysis framework tries to
automatically verify the inexistence of data races. The key challenge in doing
that is the precision of the analysis. This paper proposes an enhancement to the region analysis of Goblint to incorporate domain-specific happens-before
guarantees. The proposed addition is implemented and evaluated on the Goblint benchmark suite. We show that the given enhancement increases the precision of Goblint when analysing character drivers.
Graduation Thesis language
English
Graduation Thesis type
Master - Computer Science
Supervisor(s)
Vesal Vojdani, Kalmer Apinis
Defence year
2016