Development of parallel programs on shared data-structures – Revised version
arxiv(2024)
摘要
A syntax-directed formal system for the development of totally correct
programs with respect to an unfair shared-state parallel while-language is
proposed. The system can be understood as a compositional reformulation of the
Owicki/Gries method for verification of parallel programs. Auxiliary variables
are used both as a specification tool to eliminate undesirable implementations,
and as a verification tool to make it possible to prove that an already
finished program satisfies a particular specification. Auxiliary variables may
be of any sort, and it is up to the user to define the auxiliary structure he
prefers. Moreover, the auxiliary structure is only a part of the logic. This
means that auxiliary variables do not have to be implemented as if they were
ordinary programming variables. The system is proved sound and relatively
complete with respect to an operational semantics and employed to develop three
nontrivial algorithms: the Dining-Philosophers, the Bubble-Lattice-Sort and the
Set-Partition algorithms. Finally, a related method for the development of
(possibly nonterminating) programs with respect to four properties is
described. This approach is then used to develop Dekker's algorithm.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要