Abstract

I will present Sigma, a novel technique for learning symbolic models of software behaviour. Sigma targets synthesis of stream programs. Stream programs, consisting of interconnected filters processing sequences of data items, often have to be optimised against a variety of goals, e.g., speed, latency, throughput, etc. For instance, a compiler might want to place a ``cheap’’ filter that drops data before a ``costly’’ one that does processing, or fuse two filters when it is profitable to trade pipeline parallelism for lower communication cost. Sigma learns faithful input-output models of arbitrarily structured filters by a novel Angluin-style learning algorithm based on dynamic symbolic execution and counterexample-guided abstraction refinement. Inferred models, acting as behavioural specifications, can be effectively composed and checked for equivalence. For instance, to check whether two filters can be safely reordered we check whether the composition of inferred models commutes. In addition, the inferred models can be executed concurrently, enabling automated parallelisation of irregular loop nests that are not polyhedral, disjoint or with a static pipeline structure. In preliminary experiments, in addition to enabling optimisations of several real-world stream benchmark programs not possible with current tools, Sigma-generated models yielded on average three-fold speedups over the most optimized gcc-generated code by synthesising SIMD code using Intel SSE intrinsics (for stateless models) and GPU code using CUDA (for stateful models).