David May (computer scientist)
Encyclopedia
Michael David May, born February 24, 1951, is a British
computer scientist
. He is Professor of Computer Science at the University of Bristol
and founder and Chief Technology Officer of XMOS Semiconductor
.
May was lead architect
for the transputer. As of 2007, he holds 34 patents, all in microprocessing
and multi-processing.
, Yorkshire
, England and attended Queen Elizabeth Grammar School, Wakefield
. From 1969-1972 he was a student at King's College, Cambridge
, University of Cambridge
, initially studying Mathematics and then Computer Science in the Cambridge University Mathematical 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
microcomputer
s 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 switch
es, 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 transformation
s 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 whilst also being the Chief Technology Officer of XMOS
, a University spin-out he co-founded in 2005.
May is married with 3 sons and lives in Bristol
, United Kingdom.
, followed in 1991 by his election as a Fellow of The Royal Society and the award of the Patterson Medal of the Institute of Physics
in 1992.
In 2010, he was elected a Fellow of the Royal Academy of Engineering
.
United Kingdom
The United Kingdom of Great Britain and Northern IrelandIn the United Kingdom and Dependencies, other languages have been officially recognised as legitimate autochthonous languages under the European Charter for Regional or Minority Languages...
computer scientist
Computer scientist
A computer scientist is a scientist who has acquired knowledge of computer science, the study of the theoretical foundations of information and computation and their application in computer systems....
. He is Professor of Computer Science at the University of Bristol
University of Bristol
The University of Bristol is a public research university located in Bristol, United Kingdom. One of the so-called "red brick" universities, it received its Royal Charter in 1909, although its predecessor institution, University College, Bristol, had been in existence since 1876.The University is...
and founder and Chief Technology Officer of XMOS Semiconductor
XMOS
XMOS is a fabless semiconductor company that develops multi-core multi-threaded processors designed to execute several real-time tasks, DSP, and control flow all at once.-Company history:...
.
May was lead architect
Computer architecture
In computer science and engineering, computer architecture is the practical art of selecting and interconnecting hardware components to create computers that meet functional, performance and cost goals and the formal modelling of those systems....
for the transputer. As of 2007, he holds 34 patents, all in microprocessing
Microprocessor
A microprocessor incorporates the functions of a computer's central processing unit on a single integrated circuit, or at most a few integrated circuits. It is a multipurpose, programmable device that accepts digital data as input, processes it according to instructions stored in its memory, and...
and multi-processing.
Biography
May was born in HolmfirthHolmfirth
Holmfirth is a small town located on the A6024 Woodhead Road in the Holme Valley, within the Metropolitan Borough of Kirklees, West Yorkshire, England. Centred upon the confluence of the Holme and Ribble rivers, Holmfirth is south of Huddersfield and from Glossop. It mostly consists of...
, Yorkshire
Yorkshire
Yorkshire is a historic county of northern England and the largest in the United Kingdom. Because of its great size in comparison to other English counties, functions have been increasingly undertaken over time by its subdivisions, which have also been subject to periodic reform...
, England and attended Queen Elizabeth Grammar School, Wakefield
Queen Elizabeth Grammar School, Wakefield
Queen Elizabeth Grammar School is an independent school in Wakefield, West Yorkshire, England. QEGS is distinct from most other schools in that it was founded by Royal Charter of Queen Elizabeth I in 1591 at the request of leading citizens in Wakefield 75 in total and some of whom formed the...
. From 1969-1972 he was a student at King's College, Cambridge
King's College, Cambridge
King's College is a constituent college of the University of Cambridge, England. The college's full name is "The King's College of our Lady and Saint Nicholas in Cambridge", but it is usually referred to simply as "King's" within the University....
, University of Cambridge
University of Cambridge
The University of Cambridge is a public research university located in Cambridge, United Kingdom. It is the second-oldest university in both the United Kingdom and the English-speaking world , and the seventh-oldest globally...
, initially studying Mathematics and then Computer Science in the Cambridge University Mathematical Laboratory.
He moved to the University of Warwick
University of Warwick
The University of Warwick is a public research university located in Coventry, United Kingdom...
and started research in robotics
Robotics
Robotics is the branch of technology that deals with the design, construction, operation, structural disposition, manufacture and application of robots...
. 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
Single-board computer
A single-board computer is a complete computer built on a single circuit board, with microprocessor, memory, input/output and other features required of a functional computer. Unlike a typical personal computer, an SBC may not include slots into which accessory cards may be plugged...
microcomputer
Microcomputer
A microcomputer is a computer with a microprocessor as its central processing unit. They are physically small compared to mainframe and minicomputers...
s connected by serial communication
Serial communication
In telecommunication and computer science, serial communication is the process of sending data one bit at a time, sequentially, over a communication channel or computer bus. This is in contrast to parallel communication, where several bits are sent as a whole, on a link with several parallel channels...
links. This early work brought him into contact with Tony Hoare and Iann Barron – one of the founders of Inmos
INMOS
Inmos Limited was a British semiconductor company, founded by Iann Barron, with both the head office and the design office at Aztec West in Bristol, it was incorporated in November 1978.- Products :...
.
When Inmos
INMOS
Inmos Limited was a British semiconductor company, founded by Iann Barron, with both the head office and the design office at Aztec West in Bristol, it was incorporated in November 1978.- Products :...
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
Occam (programming language)
occam is a concurrent programming language that builds on the Communicating Sequential Processes process algebra, and shares many of its features. It is named after William of Ockham of Occam's Razor fame....
. This extended his earlier work and was also influenced by Tony Hoare, who was at the time working on CSP
Communicating sequential processes
In computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...
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 switch
Packet switch
A packet switch is a node in a network which uses the packet switching paradigm for data communication. Packet switches can operate at a number of different levels in a protocol suite; although the exact technical details differ, fundamentally they all perform the same function: they store and...
es, the C104, together with the communications system of the T9000 transputer.
Working closely with Tony Hoare and the Programming Research Group
Programming Research Group
The Programming Research Group is part of the Oxford University Computing Laboratory . It was founded by Christopher Strachey in 1965 and after his death, C.A.R. Hoare, FRS took over the leadership in 1977...
at Oxford University, May introduced formal verification techniques into the design of the T800 floating point unit
Floating point unit
A floating-point unit is a part of a computer system specially designed to carry out operations on floating point numbers. Typical operations are addition, subtraction, multiplication, division, and square root...
and the T9000 transputer. These were some of the earliest uses of formal verification
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
in microprocessor design, involving specifications, correctness preserving transformation
Program transformation
A program transformation is any operation that takes a computer program and generates another program. In many cases the transformed program is required to be semantically equivalent to the original, relative to a particular formal semantics and in fewer cases the transformations result in programs...
s and model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
, giving rise to the initial version of the FDR checker developed at Oxford.
In 1995, May joined the University of Bristol
University of Bristol
The University of Bristol is a public research university located in Bristol, United Kingdom. One of the so-called "red brick" universities, it received its Royal Charter in 1909, although its predecessor institution, University College, Bristol, had been in existence since 1876.The University is...
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 whilst also being the Chief Technology Officer of XMOS
XMOS
XMOS is a fabless semiconductor company that develops multi-core multi-threaded processors designed to execute several real-time tasks, DSP, and control flow all at once.-Company history:...
, a University spin-out he co-founded in 2005.
May is married with 3 sons and lives in Bristol
Bristol
Bristol is a city, unitary authority area and ceremonial county in South West England, with an estimated population of 433,100 for the unitary authority in 2009, and a surrounding Larger Urban Zone with an estimated 1,070,000 residents in 2007...
, United Kingdom.
Awards and recognition
In 1990, May received an Honorary DSc from the University of SouthamptonUniversity of Southampton
The University of Southampton is a British public university located in the city of Southampton, England, a member of the Russell Group. The origins of the university can be dated back to the founding of the Hartley Institution in 1862 by Henry Robertson Hartley. In 1902, the Institution developed...
, followed in 1991 by his election as a Fellow of The Royal Society and the award of the Patterson Medal of the Institute of Physics
Institute of Physics
The Institute of Physics is a scientific charity devoted to increasing the practice, understanding and application of physics. It has a worldwide membership of around 40,000....
in 1992.
In 2010, he was elected a Fellow of the Royal Academy of Engineering
Royal Academy of Engineering
-Overview: is the UK’s national academy of engineering. The Academy brings together the most successful and talented engineers from across the engineering sectors for a shared purpose: to advance and promote excellence in engineering....
.