Name
Abstract | ||
|---|---|---|
We present PORTHOS, the first tool that discovers porting bugs in performance-critical code. PORTHOS takes as input a program, the memory model of the source architecture for which the program has been developed, and the memory model of the targeted architecture. If the code is not portable, PORTHOS finds a porting bug in the form of an unexpected execution - an execution that is consistent with the target but inconsistent with the source memory model. Technically, PORTHOS implements a bounded model checking method that reduces portability analysis to the satisfiability modulo theories (SMT) problem with integer difference logic. There are two problems in the reduction that are unique to portability and that we present novel and efficient solutions for. First, the formulation of portability contains a quantifier alternation (consistent + inconsistent). We encode inconsistency as an existential query. Second, the memory models may contain recursive definitions. We compute the corresponding least fixed points efficiently in SMT. Interestingly, we are able to prove that our execution-based notion of portability is the most liberal one that admits an efficient algorithmic analysis: for state-based portability, a polynomial SAT encoding cannot exist. Experimentally, we applied PORTHOS to a number of case studies. It is able to check portability of non-trivial programs between interesting architectures. Notably, we present the first algorithmic analysis of portability from TSO to Power. |
Year | Venue | Field |
|---|---|---|
2017 | arXiv: Programming Languages | Programming language,Model checking,Axiom,Computer science,Theoretical computer science,Memory model,Software portability,Porting,Recursion,Encoding (memory),Satisfiability modulo theories |
DocType | Volume | Citations |
Journal | abs/1702.06704 | 1 |
PageRank | References | Authors |
0.35 | 15 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hernán Ponce de León | 1 | 1 | 0.35 |
| Florian Furbach | 2 | 4 | 1.75 |
| Keijo Heljanko | 3 | 751 | 47.90 |
| Roland Meyer | 4 | 203 | 15.99 |