University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Sigma*: Symbolic Learning of Input-Output Specifications

Sigma*: Symbolic Learning of Input-Output Specifications

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Peter Sewell.

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).

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity