The Computing Innovation Fellows Project

Posted on: Wednesday, May 27th, 2009
Broad Research Area: Mobile / Ubiquitous / Embedded Computing, Numerical/Scientific Computing / HPC / Data-Intensive Scalable Computing, Other, Programming Languages / Compilers, Software Engineering, Theory / Algorithms

Research Interests:

Real-world use of multi-core systems requires the development of distributed programming methods for inter-core communication. This fact is evidenced by the formation of the Multi-core association (MCA) and the development of the Multi-core Communications API (MCAPI, http://www.multicore-association.org) supported by more than 20 industrial member companies. MCAPI targets the transport layers within future multi-core SOC systems and is hoped to become the industry standard. Like the message passing interface (MPI) API for cluster computers, MCAPI is inherently complex leaving it vulnerable to ambiguity in specification, implementation, and slow adoption. To address these concerns, ensure the absence of nasty bugs, and guarantee conformance to product specifications and user expectations, we propose to employ formal specifications to characterize MCAPI; formal analysis methods to ensure that MCAPI applications are bug-free and conform to specifications; and field validation of our ideas with the help of Industrial Mentors who have expressed willingness to provide us driving examples, monitor our progress, and give feedback. The work explores technologies to improve design quality in complex APIs, facilitate multiprocessor programmability in future SOC products, and provide design verification in both hardware and software layers. In the first year we shall acquire a thorough understanding of MCAPI and other APIs such as MRAPI for resource interactions. With this understanding, we will develop a formal specification for MCAPI that can help answer putative (“what if”) queries about various scenarios of using the API. Since the uniqueness of MCAPI lies in its use of light-weight message passing in addition to shared memory consistency, understanding the formal semantics of MCAPI is crucially important. We expect this specification to help us garner valuable high level properties about MCAPI that can serve as incisive default correctness properties to verify on application codes that use MCAPI. In conjunction with the development of the formal specification, we will work on a verified golden execution model that can be used by developers to begin testing programs. The golden execution model will also serve as a reference solution for other implementations. The second year of the project is to develop dynamic execution methods that can efficiently verify MCAPI application codes directly (without model building) and also significantly reduce the number of program schedules to be examined using new partial order reduction methods. The dynamic verification engine will critically rely on the golden execution model for a runtime environment, and the partial order reduction will critically rely on the formal MCAPI specification to understand dependency relations in the API. The work in the third year of the project will be to enhance a user given test harnesses for MCAPI applications through symbolic methods thus removing the need for a closed test environment. A significant challenge to overcome in doing this generalization is how to propagate information across the API calls.

Contact Information:

http://www.cs.byu.edu/email/1903/field_contact