USTC-Yale Joint Research Center for High-Confidence Software

This project focuses on the design and implementation of the high-productivity parallel programming language, especially on synchronization, simultaneously, the program verification is in consideration.
 
                                                                             SPC-I                            SPC-II                               Publications
Research Thought
 
Our general idea about research on high-productivity parallel programming language is: programmers need to provide some simple abstract descriptions on shared resources and their usage, and these information can be used by compilers to be capable of generating high-quality codes. The high quality of codes refers to the high confidence, high efficiency, easy debugging, etc. The abstract description involves shape infomation of shared mutable data structures(such as lists, binary trees, etc), shared resources and their usage, pre and post conditions of functions, etc. The high-capacity of compilers refers to more information synthesized by program analysis, the proof of programs  satisfying specifications, the generation of proof-carrying codes, etc.
 
Research Objectives
 
Research a parallel programming language with shared resource usage declarations by solving some key theoretic and technical problems in language design, implementation, and program verification, in order to lay the groundwork for supporting easy programming on shared memory.
 
Research Content and Methods
 
Design a small parallel programming language which contains pointer type and allows the use of shared mutable data structure for study. It uses shared resource usage declarations rather than shared variable access controls in programming. Compiler can collect the holding information of shared variables from  the shared resource usage declarations in a program, then generates codes with shared variable access control based on these holding information. Besides, we extend the Rely-Guarantee method to certify these parallel programs with shared resource usage descriptions.

We carry out our work on existing infrastructure which support C program analysis and transformation, and attempt to develop a tiny language through implementing a source-to-source translator. The key problems in our research are listed below:

• Alias analysis and inference of loop invariants: Because of the existence of pointer type, it is necessary for us to consider the alias problem in the access path (expression with the form of p->front->next), obtaining the correct holding information of shared variables needs precise alias information. Precise pointer analysis depends on the loop invariants. However, it is unacceptable to require programmers provide loop invariants, and automatic inference of loop invariant is a classical problem, so far with only limited success.
• Generating efficient code for shared variable access control: To design the algorithm for generating coarse-grained lock-based code is relatively easy, but difficult in generating fine-grained lock-based code; the key point is to combine the characters of shared variables and overhead of locking operations to assign locks with appropriate granularity and locking order. However, to generate transactional memory(TM)-based code is complex because we must consider the interface between TM and complex open world including existing operating system, programming language and library code etc.
• Verification of concurrent programs with shared mutable data structure: Separation logic is the most influential logic for verifying sequential programs with shared mutable variables, while to deal with concurrent programs the logic needs to be extended. Separation logic treats the heap as several disjoint parts, and does not provide the mechanism for the link of them, thus it is difficult to express the shape characteristics of the shared mutable data structure.

Documents

• SPC-I: A Parallel Programming Language with Backward Shared Variable Holding Declaration
  • Technical Reports:
    • The version of SPC variable's type has only integer(pdf) 
  • The source-to-source implement from SPC source code to C code with lock-based access control.         
    • The SPC's compiler for int type version(spc_suifproj.tar.gz). 
    • Examples: fibonacci(fibonacci.pdf), simple producer and consumer program (pc.pdf):
      code of the examples is in the test/spc_for_integer directory of the SPC's compiler(spc_suifproj.tar.gz).
• SPC-II: A Parallel Language with Shared Resource Declaration for Mutable Data Structure
  • Technical Reports:
    • The version of SPC-II(pdf)
    • Holding analysis (pdf)
  • The source code of SPC-II translator.
    • SPC-II version(spc-II_suifproj.tar.gz).
    • Demonstration
    • SUIF2 manual (pdf)

Publications
 

• ZHANG Yu-xian, ZHANG Yu. An Automatic Approach of Fine-grained Locking for Linked Data Structure, accepted by  Journal of Chinese Computer Systems, 2011.(pdf)
• ZHANG Wei，ZHANG Yu，WANG Chen，FU Xiao-peng. An analysis approach to concurrent access control for shared mutable data, Journal of University of Science and Technology of China, 41(2): 164-172, Feb. 2011.(pdf)
• WANG Chen, ZHANG Yu, FU Xiao-peng, Zhang Wei. A parallel programming language with shared variable holding declaration, accepted by  Journal of Chinese Computer Systems, 2010.(pdf)
• FU Xiao-peng, ZHANG Yu, ZHANG Wei, WANG Chen. Study on definition-use chains algorithm in dynamic pointer-linked data structures, accepted by  Journal of Chinese Computer Systems, 2010.(pdf)
  download: source-impl.rar(33.43 KB)  benchmark.rar(include research data 443.63 KB)