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

该项目是为下一代嵌入式系统中的软件创建SHIM（软件/硬件集成介质）开发环境。 SHIM将通过使设计正确的系统更容易来提高设计人员的生产力，并通过提供软件合成来促进建筑探索。 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.