A Framework for Lightweight, Flexible and Concurrent Operating Systems

操作系统是大多数计算机系统的关键组成部分，负责管理硬件和软件。现有的操作系统，无论是商业的还是开放源码的，在功能和应用方面都有很大的不同。规模较小的是嵌入式操作系统，通常在特定应用硬件上执行高度专业化的任务（例如，控制燃油喷射汽车发动机、移动的电话或飞机导航系统的软件）。商品硬件平台（如IBM PC），存在数百万，需要更复杂的通用操作系统（Microsoft Windows和Linux是两个熟悉的例子）。规模最大的是管理大规模并行计算平台的操作系统，这些平台可能分布在网络上。无论在什么环境下使用操作系统，它都必须正确地运行并优雅地处理错误。当前的操作系统（在不同程度上）存在三个主要问题：不正确的实现：操作系统包含错误的代码，导致不期望的行为（具有从浪费时间到灾难性的影响）。缺乏可扩展性：操作系统不能扩展到单个机器或少量处理器之外，从而限制了硬件的可扩展性。缺乏表现：通常用于开发操作系统的设计和工具的性质会导致性能破坏的开销--操作系统必须确保行为不良的程序（包括操作系统本身的组件）不会无意中影响系统的其他部分。所提出的研究通过设计和开发并发操作系统组件来解决这些问题，可以简单地插在一起，以产生具有所需功能的操作系统，最初针对一系列标准化的嵌入式硬件（PC/104）。为了保证连接这些组件将按预期的方式工作，需要高度的形式主义，特别是，规范他们的并发交互。这项研究的关键方面涉及这样的网络的动态-允许组件和支持连接生成和移动，而系统仍然运行。这样的能力是有帮助的，即使是孤立的单处理器平台，但特别是有关未来的多处理器芯片和可能的总互连（无线）的普及嵌入式系统。形式主义来自两个进程代数- Hoare的CSP和米尔纳的π演算-可以描述的行为，提出的并发组件。至关重要的是，它可以揭示组合组件的精确行为，从而在设计阶段避免组件的不良组合。通过使用CSP和pi演算感知设计和编程工具，还可以保证纯顺序代码的完整性，特别是鉴于周围的concurrency.is，对允许有效利用并发性的软件技术的需求日益增加。单处理器系统正在逐渐达到其硅极限，主要制造商已经开始考虑硬件，因为故障和可持续性越来越成问题，需要采用软件设计方法。parallelism.new系统正变得越来越复杂，以至于经常延迟交付（或根本不交付），超出预算，并且在许多情况下包含未知的故障条件和行为。在许多情况下，面对不断变化的要求修改现有系统是不可行的，导致从头开始开发新系统，成本高昂，不方便。形式化的并发方法提供了可伸缩性，其成本与更改的大小成比例，而不是系统的大小。

Operating-systems are a key component of most computer systems, responsible for managing the hardware and software. Available operating-systems, both commercial and open-source, vary greatly in their capabilities and application.the small end of the scale are embedded operating-systems, often performing highly specialised tasks on application-specific hardware (e.g. the software controlling a fuel-injected car engine, mobile phone or aeroplane guidance system). Commodity hardware platforms (such as the IBM PC), of which millions exist, require more complex general-purpose operating-systems (Microsoft Windows and Linux are two familiar instances). Towards the large end of the scale are operating-systems that manage massively parallel computing platforms, possibly distributed over networks. In whatever environment an operating-system is used, it must function correctly and handle errors gracefully.current operating-systems suffer (to varying degrees) from three major problems:. Incorrect implementation: the operating-system contains erroneous code, resulting in undesirable behaviour (with effects ranging from time-wasting to catastrophic).. Lack of scalability: the operating-system fails to scale beyond a single machine or small number of processors, limiting the upgradability of the hardware.. Lack of performance: the nature of the design and tools commonly used to develop operating-systems result in performance-damaging overheads -- the operating-system must ensure that badly-behaved programs (including components of the operating-system itself) do not inadvertently affect other parts of the system.proposed research addresses these problems through the design and development of concurrent operating-system components, that can simply be plugged-together to produce operating-systems with the desired capabilities, initially targeting a range of standardised embedded hardware (PC/104). To guarantee that connecting such components will work as expected requires a high degree of formalism, in particular, specification of their concurrent interactions.crucial aspect of this research concerns the dynamics of such networks -- allowing components and supporting connections to be generated and moved around while the system still runs. Such capability is helpful even for isolated uniprocessor plaforms, but is specially relevant for future multiprocessor chips and the likely total interconnect (wireless) of pervasive embedded systems.formalism comes from two process algebras -- Hoare's CSP and Milner's pi-calculus -- that can describe the behaviour of the proposed concurrent components. Crucially, it can reveal the precise behaviour of combined components, allowing bad combinations of components to be avoided at the design stage. By using CSP and pi-calculus aware design and programming tools, guarantees can also be made about the integrity of purely sequential code, particularly in light of the surrounding concurrency.is an increasing need for software technologies that allow concurrency to be exploited efficiently. Single-processor systems are gradually reaching their silicon limits and the major manufacturers are already looking towards hardware parallelism.new approach to software design is needed, as failure and sustainability become increasingly problematic. Systems are becoming complex to a degree where they are frequently delivered late (or not at all), over-budget and, in many cases, contain unknown failure conditions and behaviours. Modifying existing systems in the face of changing requirements is unworkable in many cases, resulting in the development of new systems from scratch, at substantial cost and inconvenience. The formalised concurrent approach offers scalability at a cost proportional to the size of the change, not the size of the system.