Sigma*: Symbolic Learning of Input-Output Specifications

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

• Matko Botincan
• Monday 14 January 2013, 13:00-14:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.