Майкл Дэйвид Мэй: путь британского ученого в компьютерной науке

Введение

Британский учёный-компьютерщик Майкл Дэвид Мэй (Michael David May), член Королевского общества и Королевской инженерной академии (род. 24 февраля 1951 года) — британский учёный-компьютерщик. Он является профессором кафедры компьютерных наук Бристольского университета и основателем компании XMOS Semiconductor, где до февраля 2014 года занимал должность технического директора. Мэй был ведущим архитектором процессора Transputer. По состоянию на 2017 год он является обладателем 56 патентов в области микропроцессоров и многопроцессорных систем.

Жизнь и карьера

Мэй родился в Холмфирте, Йоркшир, Англия, и учился в школе королевы Елизаветы в Уэйкфилде. С 1969 по 1972 год он был студентом Королевского колледжа Кембриджского университета, сначала изучая математику, а затем компьютерные науки в Математической лаборатории Кембриджского университета, ныне Компьютерной лаборатории Кембриджского университета. Он перешел в Уорвикский университет и начал исследования в области робототехники. Сложности реализации систем обнаружения и управления побудили его разработать и внедрить ранний язык параллельного программирования EPL, который работал на кластере одноплатных микрокомпьютеров, соединенных последовательными каналами связи. Эта ранняя работа познакомила его с Тони Хоаром и Янном Барроном, одним из основателей Inmos. Когда Inmos была основана в 1978 году, Мэй присоединился к работе над архитектурой микрокомпьютеров, став ведущим архитектором транспондера и разработчиком связанного с ним языка программирования Occam. Эта работа стала продолжением его предыдущих исследований и также находилась под влиянием Тони Хоара, который в то время работал над CSP и выступал в качестве консультанта Inmos. Прототип транспондера назывался Simple 42 и был завершен в 1982 году. Первые серийные транспондеры, T212 и T414, появились в 1985 году, а транспондер с плавающей точкой T800 – в 1987 году. Мэй инициировал разработку одного из первых ПЛИС-пакетных коммутаторов C104, а также системы связи транспондера T9000. Тесно сотрудничая с Тони Хоаром и исследовательской группой по программированию Оксфордского университета, Мэй внедрил методы формальной верификации в разработку блока с плавающей точкой T800 и транспондера T9000. Это было одним из первых применений формальной верификации в проектировании микропроцессоров, включающее спецификации, преобразования, сохраняющие корректность, и проверку моделей, что привело к созданию первоначальной версии FDR-проверщика, разработанного в Оксфорде. В 1995 году Мэй присоединился к Бристольскому университету в качестве профессора информатики. С 1995 по 2006 год он был заведующим кафедрой информатики. Он продолжает работать профессором в Бристоле, поддерживая XMOS, спин-офф университета, который он основал в 2005 году. До XMOS он участвовал в работе Picochip, где написал оригинальный набор инструкций. Мэй женат, имеет троих сыновей и проживает в Бристоле, Великобритания.

May was born in Holmfirth, Yorkshire, England and attended Queen Elizabeth Grammar School, Wakefield. From 1969 to 1972 he was a student at King's College, Cambridge, University of Cambridge, at first studying Mathematics and then Computer Science in the University of Cambridge Mathematical Laboratory, now the University of Cambridge Computer Laboratory. He moved to the University of Warwick and started research in robotics. The challenges of implementing sensing and control systems led him to design and implement an early concurrent programming language, EPL, which ran on a cluster of single board microcomputers connected by serial communication links. This early work brought him into contact with Tony Hoare and Iann Barron: one of the founders of Inmos. When Inmos was formed in 1978, May joined to work on microcomputer architecture, becoming lead architect of the transputer and designer of the associated programming language Occam. This extended his earlier work and was also influenced by Tony Hoare, who was at the time working on CSP and acting as a consultant to Inmos. The prototype of the transputer was called the Simple 42 and was completed in 1982. The first production transputers, the T212 and T414, followed in 1985; the T800 floating point transputer in 1987. May initiated the design of one of the first VLSI packet switches, the C104, together with the communications system of the T9000 transputer. Working closely with Tony Hoare and the Programming Research Group at Oxford University, May introduced formal verification techniques into the design of the T800 floating point unit and the T9000 transputer. These were some of the earliest uses of formal verification in microprocessor design, involving specifications, correctness preserving transformations and model checking, giving rise to the initial version of the FDR checker developed at Oxford. In 1995, May joined the University of Bristol as a professor of computer science. He was head of the computer science department from 1995 to 2006. He continues to be a professor at Bristol while supporting XMOS, a University spin out he co founded in 2005. Before XMOS, he was involved in Picochip, where he wrote the original instruction set. May is married with three sons and lives in Bristol, United Kingdom.

Награды и признание

В 1990 году Мэй получил почетную степень доктора наук (DSc) от Университета Саутгемптона, после чего в 1991 году был избран членом Королевского общества, а в 1992 году удостоен медали и премии Клиффорда Патерсона Института физики. В 2010 году он был избран членом Королевской инженерной академии.