Resource Reasoning

资源推理

基本信息

批准号：
EP/H008373/2
负责人：
Peter O'Hearn
金额：
$ 284.06万
依托单位：
University College London
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2012
资助国家：
英国
起止时间：
2012 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FH008373%2F2
关键词：
Resource Reasoning

项目摘要

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.

资源一直是计算机系统中的核心问题。例如，在经典操作系统中，流程访问系统资源，例如内存，锁，文件，处理器时间和网络带宽；正确的资源使用对于系统的整体工作至关重要。在万维网中，整个结构可以被视为一个巨大的，动态的资源网，其统一的资源识别仪指的是定期的数据和代码。通常，对于各种计算机系统，程序员仔细考虑系统处理资源作为手头编程任务的一部分是第二天性。这项研究的观点是，我们称之为一种新颖的数学理论，我们称之为资源推理，它与程序员对资源的非正式思考息息相关。这种理论的第一阶段是分离逻辑及其亲戚的代表，这些发展暗示了更多。我们的假设是，就像“面向资源的思维”在正式系统设计中占据中心位置一样，资源也是对现代和未来计算基础架构的计划的正式分析和验证的核心。面临的挑战是发展一种资源推理的优雅理论（或理论），该理论都与程序员和系统设计师的非正式直觉相吻合，并为一系列问题域，例如经典操作系统，诸如经典操作系统，诸如经典操作系统，诸如经典操作系统的验证和验证技术提供了可易处理的分析和验证技术。持续不断发展的Web软件，并发编程甚至硬件合成。该项目将提供新的理论概念和新的原型工具，最终将有助于使计算机崩溃的频率降低，不频繁地崩溃，并且通常会提高可靠性。