Dead code elimination based pointer analysis for multithreaded programs

TL;DR

This paper introduces a new type-based pointer analysis and dead code elimination method for multithreaded programs, enabling certified optimizations with formal correctness proofs.

Contribution

It presents a novel operational semantics for multithreaded constructs and a type system that supports flow-sensitive pointer analysis, live-variable analysis, and dead code elimination with formal justification.

Findings

New operational semantics for parallel constructs

Type system for flow-sensitive pointer analysis

Type system for dead code elimination with proof-carrying capability

Abstract

This paper presents a new approach for optimizing multitheaded programs with pointer constructs. The approach has applications in the area of certified code (proof-carrying code) where a justification or a proof for the correctness of each optimization is required. The optimization meant here is that of dead code elimination. Towards optimizing multithreaded programs the paper presents a new operational semantics for parallel constructs like join-fork constructs, parallel loops, and conditionally spawned threads. The paper also presents a novel type system for flow-sensitive pointer analysis of multithreaded programs. This type system is extended to obtain a new type system for live-variables analysis of multithreaded programs. The live-variables type system is extended to build the third novel type system, proposed in this paper, which carries the optimization of dead code elimination. The justification mentioned above takes the form of type derivation in our approach.