Published by

Last news

Invited Speakers

Keynote Talks by Steve Furber and Yosinori Watanabe.

Deadline extended

Deadline for submissions of papers extended until 17 january 2009.

Last call for papers

Please note the extended deadline for paper submission.

Conference hompage online

Please note the important dates and the preliminary call for papers.

Steve Furber: Biologically-Inspired Massively-Parallel Architectures - computing beyond a million processors

Gerhard Schellhorn: Formal Verification of Lock-Free Algorithms

Yosinori Watanabe: Examining important corner cases: verification of interacting architectural components in system designs

Steve Furber: Biologically-Inspired Massively-Parallel Architectures - computing beyond a million processors

The SpiNNaker project aims to develop parallel computer systems with more than a million embedded processors. The goal of the project is to support large-scale simulations of systems of spiking neurons in biological real time, an application that is highly parallel but also places very high loads on the communication infrastructure due to the very high connectivity of biological neurons. The scale of the machine requires fault-tolerance and power-efficiency to influence the design throughout, and the development has resulted in innovation at every level of design, including a self- timed inter-chip communication system that is resistant to glitch-induced deadlock and 'emergency' hardware packet re-routing around failed inter-chip links, through to run-time support for functional migration and real-time fault mitigation.

CV of Steve Furber

Professor Stephen Byram Furber is the ICL Professor of Computer Engineering at the School of Computer Science at the University of Manchester. He is probably best known for his work at Acorn where he was one of the designers of the BBC Micro and the ARM 32-bit RISC microprocessor.

Furber was educated at Manchester Grammar School and represented the UK in the International Mathematical Olympiad in Hungary in 1970. He went up to Cambridge and received a BA in mathematics in 1974. In 1978, he was appointed the Rolls-Royce Research Fellow in Aerodynamics at Emmanuel College, Cambridge and was awarded a PhD in 1980.

From 1980 to 1990, Furber worked at Acorn Computers Ltd where he was a Hardware Designer and then Design Manager. He was a principal designer of the BBC Micro and the ARM microprocessor.

In August 1990 he moved to the Victoria University of Manchester to become the ICL Professor of Computer Engineering and established the Amulet research group.

Professor Furber's latest project is known as Spinnaker, also nicknamed the 'brain box', to be constructed at the University of Manchester. This is an attempt to build a new kind of computer that directly mimics the workings of the human brain. Spinnaker is essentially an artificial neural network realised in hardware, a massively parallel processing system eventually designed to incorporate a million ARM processors. The finished Spinnaker will model 1% of the human brain's capability, or around 1 billion neurons.

Furber is a Fellow of the Royal Academy of Engineering, of the Royal Society, the IEEE and the Institution of Engineering and Technology, and is a Chartered Engineer. He is on the Advisory Board of Theseus Logic, Inc.

Furber's research interests include asynchronous systems, ultra-low-power processors for sensor networks, on-chip interconnect and GALS (Globally Asynchronous Locally Synchronous), and neural systems engineering.


Gerhard Schellhorn: Formal Verification of Lock-Free Algorithms

The current trend towards multi-core processors has renewed the interest in the development and correctness of concurrent algorithms. Most of these algorithms rely on locks to protect critical sections from unwanted interference. Recently a new class of nonblocking algorithms has been developed which do not rely on critical sections, but on atomic compare-and-set instructions. Such lock-free algorithms are less vulnerable to the typical problems of concurrent algorithms: deadlocks, livelocks and priority inversion. On the other hand, the lack of a uniform principle to rule out interference results in increased complexity. This makes it harder to understand these algorithms and to verify their correctness. The talk will use a simple example to demonstrate the central correctness criteria of linearizability (a safety property) and lock-freeness (a liveness property) for lock-free algorithms. I will then discuss our approach to the modular verification of lock-free algorithms which uses rely-guarantee reasoning and a powerful temporal logic to derive proof obligations that can be verified with the interactive theorem prover KIV. Finally I will give an overview over techniques that are relevant to automate proofs.

CV of Gerhard Schellhorn

Dr. Gerhard Schellhorn leads the Formal Methods Group at the Institute of Software and Systems Engineering (ISSE) in Augsburg headed by Prof. Reif.

He studied Computer Science at the University of Karlsruhe. He then worked as a researcher at the Universities of Karlsruhe and Ulm, where he received his PhD in 2001 on the formal verification of a Prolog compiler.

Schellhorn's general area of interest is the use formal methods in Software Engineering. He has worked on formal safety analysis for embedded systems, security analysis of smartcard applications, and developed a formal refinement theory for Abstract State Machines. He also contributed to the development of the interactive theorem prover KIV.


Yosinori Watanabe: Examining important corner cases: verification of interacting architectural components in system designs

In embedded system design, design errors are often introduced at the interfaces between multiple architectural components. Systematic design methodology for verifying the interaction between the components is imperative for improving the design productivity. In practice, different kinds of interactions need to be examined, in terms of levels of abstraction and in terms of types of architectural components. In all the cases, the key aspect is to stress the interacting components in such a way that important corner cases can be effectively examined, but the models to be used and the issues to be addressed vary, depending upon the kinds of interactions to be verified. In this talk, we observe typical types of interactions one needs to examine in embedded system designs, and present issues and requirements that one needs to account for. We then show some approaches that can be used for the interaction verification, and discuss how the stated requirements are addressed with those approaches.

CV of Yosinori Watanabe

Yosinori Watanabe is Research Scientist at Cadence Research Laboratories in Berkeley.

He received the M.S. and Ph.D. degrees in Electrical Engineering and Computer Sciences from University of California at Berkeley in 1991 and 1994.

Yosinori's current areas of interest are methodology and automation for embedded system design. Most of his recent work is conducted under the Metropolis project, where he contributes to defining the mechanism of modeling key aspects of embedded system design such as architecture components or refinement, defining abstraction levels to capture design for multi-media and mobile communication applications, as well as synthesis tool sets for hardware and software implementations respectively. An article published in IEEE Computer Magazine in April 2003 provides a brief overview of the Metropolis modeling mechanisms.

Prior to the work on system design, Yosinori worked on logic synthesis for high-performance circuits. He contributed to developing a synthesis procedure that efficiently accounts for a large number of possible implementations during technology mapping. A good summary of this work is found in the article he published in IEEE Transactions on CAD in August 1997.