Collaborative Research: Formal Analysis of Multicore Communication APIs and Applications

“该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。“CCF - 0903408协作研究- MCDA：多核通信API和应用程序的形式化分析Gopalakrishnan，Ganesh L. 犹他州大学CCF - 0903491合作研究：多核通信API和应用程序的形式化分析。 杨百翰大学ABSRTACT这个项目有助于工具工程师未来的信息处理系统，使他们可靠和有效地运行。考虑到这些系统中的许多将在单个微芯片上生产，并且考虑到对设计的快速周转时间的需求不断增加，制造商正在标准化这些芯片中的中央处理单元可以通信的方法。这些标准将消除重复劳动，并允许来自不同制造商的组件混合和匹配。 由于这些标准将管理数百万未来系统的构建，因此必须应用严格的工程原理，并辅之以数学上合理的分析方法，以确保这些标准没有缺陷。这是该项目的重要目标之一。 其他关键目标是确保这些系统的制造按照标准定义进行，并及时采用测试方法来检查制造的正确性。主要研究人员的互补优势，其中一人来自湖城犹他州大学计算机学院，另一人来自普罗沃犹他州的杨百翰大学，将有助于以独特的方式推动该项目向前发展。该项目的第一年将研究称为MCAPI的标准的严格规范方法。第二年将涉及使用MCAPI编写的程序的各种分析工具的研究设计。第三年将在系统芯片制造商现场对我们的工具进行试点测试。

"This award is funded under the American Recovery and Reinvestment Act of 2009(Public Law 111-5)."CCF - 0903408 Collaborative Research - MCDA: Formal Analysis of Multicore Communication APIs and ApplicationsGopalakrishnan, Ganesh L. University of Utah CCF - 0903491 Collaborative Research: Formal Analysis of Multicore Communication APIs and ApplicationsMercer, Eric G. Brigham Young UnivABSRTACTThis project contributes tools to engineer future information processing systems so that they operate reliably and efficiently. Given that many of these systems will be produced on single micro-chips, and given the increasing demands for rapid turn-around times of designs, manufacturers are standardizing on methods by which the central processing units in these chips may communicate. Such standards will eliminate duplication of labor and allow components originating from different manufacturers to be mixed and matched. Since such standards will govern the construction of millions of future systems, one has to apply rigorous engineering principles accompanied by mathematically sound analysis methods to ensure that the standards are not flawed. This is one of the important goals of this project. The other key goals are to ensure that the manufacturing of these systems proceeds as per the standard definition and that testing methods to check the correctness of manufacture will be in place in a timely manner. The complementary strengths of the principal investigators, one of whom is from the School of Computing, University of Utah, Salt Lake City, and the other from Brigham Young University in Provo Utah will help drive this project forward in unique ways. The first year of this project will investigate rigorous specification methods for this standard called MCAPI. The second year will involve the research design of a variety of analysis tools for programs written using MCAPI. The third year will involve pilot testing of our tools at the manufacturer sites of systems on chips.