CSR---EHS: SHIM: Developing Embedded Systems with Deterministic Concurrency

该项目正在为下一代嵌入式系统中的软件创建SHIM(软件/硬件集成介质)开发环境。Shim将通过更容易地设计正确的系统来提高设计人员的工作效率，并将通过提供软件合成来促进架构探索。填充计算模型通过可靠的通信提供确定性并发，简化了验证，因为行为是可重现的。基于通过集合通道通信的异步并发进程，SHIM可以处理控制、多速率和可变速率数据流以及与数据相关的决策。SHIM语言将为设计者提供一种正确的构造方法来描述并发系统。基于正式的语义，Shim确保系统符合模型，这是通过向现有语言添加库很难确保的。一个高效的垫片模拟器将允许在硬件可用之前对软件进行模拟。由于其决定论，Shim保证了模拟行为和最终实现之间的保真度。软件合成系统将生成在现有环境(如实时操作系统)中工作的C语言。这样做的目标是可配置性(例如，提供对作为中断例程实现的内容的控制)、性能和大小优化。正式的分析工具将静态地预测死锁、预测性能瓶颈，并识别其他设计问题。由于Shim是有限状态的，且具有相当高的层次，因此对Shim系统进行形式化分析是可行的。与任何编程系统一样，开发人员需要库来最有效地使用Shim。促进这类库将是语言设计的一个主要重点；这类库将作为该项目的一部分创建。

This project is creating the SHIM (software/hardware integration medium) development environment for the software in next-generation embedded systems. SHIM will improve designer productivity by making it easier to design correct systems and will facilitate architectural exploration by providing software synthesis. The SHIM model of computation provides deterministic concurrency with reliable communication, simplifying validation because behavior is reproducible. Based on asynchronous concurrent processes that communicate through rendezvous channels, SHIM can handle control, multi- and variable-rate dataflow, and data-dependent decisions.The SHIM language will give designers a correct-by-construction way to describe concurrent systems. Based on a formal semantics, SHIM guarantees systems comply with the model, something that would be difficult to ensure by adding a library to an existing language. An efficient simulator for SHIM will allow software to be simulated before hardware is available. Because of its determinism, SHIM guarantees fidelity between simulated behavior and the final implementation. A software synthesis system will generate C that works within existing environments such as real-time operating systems. The goals of this are configurability, (e.g., providing control over what is implemented as an interrupt routine) performance, and size optimization. A formal analysis tool will statically predict deadlocks, predict performance bottlenecks, and identify other design problems. Since SHIM is finite-state and fairly high level, formal analysis of SHIM systems is practical. Like any programming system, developers need libraries to use SHIM most efficiently. Facilitating such libraries will be a major focus of the language design; such libraries will be created as part of this project.