Using mathematics to better specify and design computer systems - Think Kent video

As part of the University of Kent Think Kent series – a collection of YouTube videos celebrating research with international impact at the University – Mark Batty explores how mathematics can improve computer systems.

Modern computer systems have intricate and unusual memory behaviour. As a result, it can be dangerous to use intuition, specifications are universally unreliable, and the outcome of testing is both profoundly unlikely to provide complete coverage and dependent on hardware that is getting more permissive of odd behaviour with each generation. These complications pervade the whole system, and have led to bugs in language specifications, deployed processors, compilers, and vendor-endorsed programming idioms – it is clear that current engineering practice is severely lacking.

Dr Mark Batty tackles these problems by developing rigorous mathematical specifications, testing tools, and verification techniques for real-world concurrent systems, focusing on established interfaces (e.g. C, C++ and, OpenCL) and concrete testable artefacts (e.g. x86, Power, ARM CPUs, and Nvidia, AMD GPUs). His interests span a variety of complementary topics including: empirical testing of the behaviour of hardware and compilers, building formal models of parts of the system, the development of algorithms and data-structures that use fine-grained concurrency, and the verification of those pieces of concurrent code.

Prior to coming to Kent, Mark completed his PhD at Cambridge and worked in Nvidia Corporation. Mark is a Lloyds Register Foundation and Royal Society of Engineering Research Fellow, and he has received awards from both the British Computing Society and the Association of Computing Machinery Special Interest Group on Programming Languages.