Parallel Programming Language with Requirement Description of Shared Resources
(Chinese Version)
This project is a sub-project of Synchronization Mechanisms in Parallel Programming,
and focuses on the design and implementation of the high-productivity parallel programming language, at
the same time, the program verification is in consideration.
Research Thought
Our general idea about research on high-productivity parallel programming language is: in parallel programming,
it is easier to generate high-quality codes when programmers provide some simple abstract descriptions. This
information can be used by the compilers to enhance their own capacity. The high quality of codes refers to
the high confidence, high efficiency, easy debugging, etc. The abstract description is about shared mutable
data structure, pointer fields which are accessed and updated through pointers (such as lists, binary trees,
etc), information about shared resource, pre and post conditions of functions, etc. The high-capacity of
compilers refers to the more information synthesized by program analysis, the proof of programs¡¯ satisfied
specifications, the generation of proof-carrying codes, etc.
Research Objectives
Research a parallel programming language with requirement description of shared resources by solving some
key theoretic and technical problems in language design, implementation, and program verification, to lay
the groundwork for supporting easy programming on shared memory.
Research Content and Methods
Design a small parallel programming language which contains the pointer type and allows the use of shared
mutable data structure for study. It uses shared resource descriptions rather than shared variable access
control in programming. In the shared resource description, we collect the maintenance section (the section
that shared variables cannot be accessed by other threads) of each shared variable, then generate codes with
shared variable access control based on these sections. Besides, we extend the
Rely-Guarantee method to certify these
parallel programs with shared resource description.
We will 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 maintenance sections of shared variables needs the
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 only limited success. Therefore, we attempt to reduce the difficulty of
program analysis by requiring programmer to provide some extra declaration information (such as the shape
of the pointed data structure, the pre- and post- condition of functions).
- Generating efficient code for shared variable access control: To design the algorithm for
generating lock-based code is relatively easy; 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. We will continue
to deepen the research on the various operational semantics of TM, the interaction semantics between
transactional and non-transactional code etc. This is the basic requirement for coming out with the
conditions of generating transactional code for programs written with our proposed language.
- 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 needs for further extension of the logic. 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.
Pointer Logic is also an exclusive logic for verifying programs using pointers, its advantages are
the easiness and convenient for portraying a variety characteristics of shared mutable data structure,
while its drawback is that it is still complex to verify a programs with the rules of pointer logic,
because the inference rules require the complex alias calculus.