Campus Event Calendar
Event Entry
What and Who
Baltic: Service Combinators for Farming Virtual Machines
Andrew D. Gordon
Microsoft Research
SWS Distinguished Lecture Series
Andrew D. Gordon is a Principal Researcher at Microsoft Research, Cambridge. Before joining Microsoft in 1997, Gordon was a Royal Society University Research Fellow at the University of Cambridge Computer Laboratory. He holds degrees in Computer Science from the University of Edinburgh and the University of Cambridge. As a postdoc, he was a member of the Programming Methodology Group at Chalmers University in Gothenburg. Gordon's research interests are in the general area of computer programming languages. He is the co-inventor of two influential process calculi: the spi calculus (with M. Abadi) and the ambient calculus (with L. Cardelli). His recent work focuses on applying type theory and other formal techniques to problems of computer security. For example, the Samoa Project (with K. Bhargavan and C. Fournet) is developing formal tools for the security of XML Web Services.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 20 November 2007
14:00
60 Minutes
G26
bldg. 57, rotunda
Kaiserslautern
Abstract
Based on joint work with
Karthikeyan Bhargavan, Microsoft Research
Iman Narasamdya, University of Manchester
We consider the problem of managing server farms largely automatically, in software. Automated management is gaining in importance with the widespread adoption of virtualization technologies, which allow multiple virtual machines per physical host. We consider the case where each server is service-oriented, in the sense that the services it provides, and the external services it depends upon, are explicitly described in metadata. We describe the design, implementation, and formal semantics of a library of combinators whose types record and respect server metadata. Our implementation consists of a typed functional script built with our combinators, in control of a Virtual Machine Monitor hosting a set of virtual machines. Our combinators support a range of operations including creation of virtual machines, their interconnection using typed endpoints, and the creation of intermediaries for tasks such as load balancing. Our combinators also allow provision and reconfiguration in response to events such as machine failures or spikes in demand. We describe a series of programming examples run on our implementation, based on existing server code for order processing, a typical data centre workload. To obtain a formal semantics for any script using our combinators, we provide an alternative implementation of our interface using a small concurrency library. Hence, the behaviour of the script plus our libraries can be interpreted within a statically typed process calculus. Assuming that server metadata is correct, a benefit of typing is that various server configuration errors are detected statically, rather than sometime during the execution of the script.
Karthikeyan Bhargavan, Microsoft Research
Iman Narasamdya, University of Manchester
We consider the problem of managing server farms largely automatically, in software. Automated management is gaining in importance with the widespread adoption of virtualization technologies, which allow multiple virtual machines per physical host. We consider the case where each server is service-oriented, in the sense that the services it provides, and the external services it depends upon, are explicitly described in metadata. We describe the design, implementation, and formal semantics of a library of combinators whose types record and respect server metadata. Our implementation consists of a typed functional script built with our combinators, in control of a Virtual Machine Monitor hosting a set of virtual machines. Our combinators support a range of operations including creation of virtual machines, their interconnection using typed endpoints, and the creation of intermediaries for tasks such as load balancing. Our combinators also allow provision and reconfiguration in response to events such as machine failures or spikes in demand. We describe a series of programming examples run on our implementation, based on existing server code for order processing, a typical data centre workload. To obtain a formal semantics for any script using our combinators, we provide an alternative implementation of our interface using a small concurrency library. Hence, the behaviour of the script plus our libraries can be interpreted within a statically typed process calculus. Assuming that server metadata is correct, a benefit of typing is that various server configuration errors are detected statically, rather than sometime during the execution of the script.
Contact
Brigitta Hansen
0681 - 9325200
--email hidden
passcode not visible
logged in users only
Brigitta Hansen, 11/09/2007 14:45 -- Created document.