Proof Method And Application Of Deterministic Parallel Programming Model

It is a research hotspot to develop parallel programs and gurantee the correctness. Due to the indeterminacy of thread interleaving order, it is hard to cover all executions of parallel programs in testing, and to reproduce bugging executions in debugging. Thus it is hard to guarantee the correctness of programs even testing and debugging massively, the deterministic parallelism technology ensures that results of all exectuions are the same and bugging executions can always be reproduced. Thus testing and debugging works can be simplified.In present, existing perspective about parallel determinism is not unified and has deficiency as instructions in testing and debugging. Taking a shared-message-channel-based parallel programming model as example, the paper researches what is determinism, how to prove it and how to offer better instructions to testing and debugging works.In all, this paper discusses and completes the following works:1. To provide a better perspective about different determinismThe paper points out that the key differences of various determinism are selecting different program points to observe at and how to observe the program state. It is subjective choices to select combinations, corresponding different determinism. It is objective that a program satifies specific determinism, and that depends on the semantics of the program and the memory model.A program is deterministic corresponding to two chosen factors, if and only if two arbitrary executions of the program have the same ability to reach the specific program point,(both of them can reach the point or neither, two situation are opposite), and (if they can) the program states while reaching the points are the same under observation.For example, final determinism means to observe the whole program state at the final program point of executions, while debugging determinism means to observe the relative part of program state of debugging thread at breakpoints.2. To provide a general proof framework of determinism, and to apply the framework to a shared-message-channel-based programming model SPMC, and to prove final determinism and debugging determinism of the model. This paper selects a deterministic parallel programming model SPMC as study object. Based on the abstract syntax, program state and operational semantics, two kinds of determinism are defined and proved, which instruct the testing and debugging works. It is difficult to understand the mixture of complicated formalized model and the determinism proof. So the paper presents in such a way, that at first a simple enough deterministic pattern is presented to show the general proof framework of determinism of model, then applies the framework in SPMC model.In brief, the perspective about determinism in this paper is more general and instructs the testing and debugging works better, and the proof is helpful to similar relative works.