Principled, Retargetable, Ultra-High Performance Automated ISA Testing
Fully funded PhD studentship available now!
This project combines recent progress in software testing (e.g. coverage guided greybox fuzzers, explosion in SMT-solver performance, self-composition for hyper property testing) ISA specification (e.g. rise of rigorous ISA specification DSLs such as Sail and ASL) and high-performance ISA emulation (e.g. GenSim), into a unified whole for automated ISA testing. We propose testing of information flow properties as an especially demanding use case.
Over the last few years, we’ve seen the convergence of multiple developments at the hardware / software boundary that make research on principled, retargetable ISA testing highly promising. Those include:
- Slowing down of Moore’s law, and a concomitant rise in demand for domain specific processors and accelerators.
- Increasing pressure on lowering the time from idea to taped-out silicon, which can only be met with more automation and higher-performance from tooling such as testers and emulators.
- Novel security demands, arising from new compute tasks such as virtualisation in the cloud and new security threats, in particular side channels and micro- architectural attacks, such as Spectre.
- The hardening divide between ISA-level modelling and micro-architectural modelling, witnesses by the rise of domain-specific languages for either, e.g. Arm’s ASL and Sail for the former and Chisel, FIRRTL, LLHD for the latter.
- Increasing rigour in ISA specification, for example: Sail is rigorously formally defined, which enables and simplifies the principled automated construction of test cases, and automatic generation of notions of test coverage. Sail, unlike previous ISA specification languages, has an expressive typing system (called liquid types), and it should be possible to use types to improve automatic test generation.
- Strong demand for crossing the hardware/software chasm, for example witnessed by intense memory model verification).
- Desire of integration of verification tool chains at hardware/software boundary to deal with cross-cutting issues (e.g. memory models, security properties)
- An explosion in software testing methodology (e.g. property based testing) and tooling: in particular, large-scale automated software testing has progress in in leaps and bounds with the rise of Coverage-guided greybox fuzzers and explosion in SMT-solver performance.
- Availability of much more compute resources that makes ultra-large scale automated testing more feasible, see e.g. Google’s cloud fuzzing.
It is time to tie those thread together make a grand jump in better automated ISA testing, in order to achieve:
- Higher performance (speed, coverage)
- Higher degree automation
- More complicated properties being tested
- Better integration with tooling pipeline
Students interested in pursuing a PhD in the above area are invited to contact me.