PI: Greta Yorsh, RA: Julian Nagele, Queen Mary, University of London, PhD Student: Maria A. Schett, University College London
- Optimising compilers for Single-Instruction-Multiple-Data (SIMD) architectures rely on sophisticated program analyses and transformations.
- Correctness hard to prove due to interaction between optimisation passes and SIMD semantics/costs.
- Supervectorizer: integration of unbounded superoptimization with auto-vectorisation enables software to take full advantage of SIMD capabilities of existing and new microprocessor designs.
- Potential for fundamental advances in SMT solvers and industrial-strength SIMD optimising compilers
The original aim of the project was to apply unbounded superoptimization to the problem of generating SIMD code. This approach results in faster code than what can be generated using traditional compiler optimization technique called vectorization. With this approach, the problem is encoded in first-order constraints and solved using an SMT solver which has to be extended with special heuristics.
As a prerequisite, the PI started the theoretical development of a framework for symbolic cost models of modern compute architecture, targeting ARM8 as the first experimental platform. The RA supported by this grant, Julian Nagele, worked on the improvement of the initial prototype to make it more reconfigurable and extensible, and evaluation on small, but important benchmarks.
Unfortunately, the PI had substantial health problems, and could not continue to be involved in the work. Without the support of the PI, the RA was not able to carry out the work on SIMD code generation, which required expert knowledge of vectorization, ARM architecture, and SMT solvers.
However, the RA realised the potential of applying this technology to smart contracts. He took a leading role on this research, identifying the direction of blockchain, and brought the work to completion. The PI provided high-level guidance, but was not actively involved in this work. The RA independently established a collaboration at UCL with a group interested in start contracts verification, which motivated this work on optimization. The paper has been accepted for publication at LOPSTR’19.
The reviewers recognised the importance of the application domain of smart contracts, novelty of superoptimization in this context, the extensive specification and benchmarking produced by the authors. Upon completion of this project, the PI has gone on to work at the global proprietary trading firm Jane Street, whereas the RA has gone on to work at Bank of America.
PUBLICATIONS. Julian Nagele, Maria A. Schett. “Blockchain Superoptimizer.” LOPSTR 2019.
RELATED GRANTS. Dr Greta Yorsh, ERC Starting Grant, £1.25M, 2018-2022.
IMPACT. The prototype and benchmarks are available as open-source. The RA and the PhD student are preparing a journal version of the paper. Recently, there has also been interest in this prototype from industry.
