Resource Reasoning

Lead Research Organisation: University College London
Department Name: Computer Science

Abstract

Resource has always been a central concern in computer systems. In classical operating systems for example, processes access system resources such as memory, locks, files, processor time, and network bandwidth; correct resource usage is essential for the overall working of the system. In the World Wide Web, the whole structure can be regarded as a giant, dynamic resource net, with its Uniform ResourceIdentifiers referring to located data and code. Generally, for all kinds of computer system, it is second nature for a programmer to think carefully about the way the system handles resource as part of the programming task in hand. The point of view of this research is that there can be a novel kind of mathematical theory, which we call resource reasoning, which goes hand in hand with programmers' informal thinking about resources. The first stage of such a theory is represented by Separation Logic and its relatives, developments which are suggestive of much more. Our hypothesis is that, just as `resource-oriented thinking' occupies a central position in pre-formal system design, resource is also central to the formal analysis and verification of programs across the modern-day and future computing infrastructure. The challenge is to develop an elegant theory (or theories) of resource reasoning, that both meshes with programmers' and system designers' informal intuitions, and leads to tractable analysis and verification techniques for a range of problem domains such as classic operating systems, the continually-evolving web software, concurrent programming, and even hardware synthesis.The project will provide new theoretical concepts and new prototype tools that will eventually help to make computers that crash less frequently, mishandle our data less frequently, and generally have improved reliability.

Publications

10 25 50

Related Projects

Project Reference Relationship Related To Start End Award Value
EP/H008373/1 01/01/2010 01/03/2012 £3,189,258
EP/H008373/2 Transfer EP/H008373/1 01/03/2012 30/06/2016 £2,248,640
 
Description This project has been about local reasoning about resources. It arose from work on various forms of separation logic and its associated automatic verification tools for computer programs. The ongoing project is to develop an elegant theory (or theories) of resource reasoning that meshes with programmers' informal intuitions and leads to tractable analysis and verification techniques for a range of problem domains, such as classic operating systems, the evolving world of web software, and concurrent programming.
Exploitation Route The ideas developed in this project are contributing to new project proposals in areas diverse as distributed systems and reasoning about security policies in human-centred organizations.

Several members of the project (or people associated with the project) are now working with major companies, including Amazon, Facebook, and Google, where ideas from this project are directly impacting upon major R&D projects.
Sectors Digital/Communication/Information Technologies (including Software)

URL http://www.resourcereasoning.com
 
Description Influence on program analysis and verification operations in Facebook and Amazon.
First Year Of Impact 2013
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Economic

 
Description Facebook Faculty Grant to James Brotherston 2015
Amount $30,000 (USD)
Organisation Facebook 
Sector Private
Country United States
Start 10/2015 
End 09/2018
 
Title CYCLIST 
Description : Generic cyclic theorem prover, instantiation to symbolic-heap separation logic plus associated tools for same 
Type Of Material Improvements to research infrastructure 
Year Produced 2014 
Provided To Others? Yes  
Impact Regularly cited in the academic literature on theorem proving and separation logic. 
URL https://github.com/ngorogiannis/cyclist
 
Title julia systems modelling package 
Description Packages for the julia (www.julialang.org) modelling languages that capture our systems and security modelling approach. Presentation in progress. 
Type Of Material Improvements to research infrastructure 
Year Produced 2016 
Provided To Others? Yes  
Impact Presentations at the UK Research Institute in the Science of Cybersecurity (RISCS) first-phase final meeting. http://www.riscs.org.uk/?page_id=15 
URL https://github.com/tristanc/SysModels
 
Description Collaboration with INRIA and Université de Lorraine 
Organisation The National Institute for Research in Computer Science and Control (INRIA)
Country France 
Sector Public 
PI Contribution Research collaboration in theory of substructural modal logics and their application in systems and security modelling.
Collaborator Contribution Research collaboration in theory of substructural modal logics and their application in systems and security modelling.
Impact J.-R. Courtault, D. Galmiche, and D. Pym. A Logic of Separating Modalities. Accepted for publication in Theoretical Computer science, subject to minor revisions. Further research and publications are ongoing.