Semantics Equivalence Of Concurrent Data-Race-Free Programs

Multicore processors have become the majority of proccessors,which makes con-current programming the majority of current programming.Concurrent programs can take fill advantages of multicore processors,and they have better performance than se-quential programs.However,programmers meet great difficulties to reason about the behaviors of concurrent programs because of the non-determ inistic interleaving execu-tion.Therefore,concurrent programs usually have more bugs than sequential programs.It is very important to ensure the correctness of concurrent programs,which has been a popular topic in program verification and formal methods for years.One of the greatest obstacles in the verification of concurrent programs is the non-deterministic interleaving execution and the exponential number of possible interleav-ings.To simplify the reasoning,we propose a non-preemptive semantics for data-race-free(DRF)concurrent programs,where a thread yields the control of the CPU only at certain carefully-chosen program points.Non-preemptive semantics greatly reduces the interleaving we need to consider,thus making the verification process much simpler.This thesis studies the semantics equivalence of standard preemptive semantics and non-preempitve semantics for data-race-free concurrent programs.In this way,we can study the behavior of concurrent programs under non-preemptive semantics instead of preemptive semantics,which will help reducing the complexity of verification.This thesis makes the following contributions:· We present a simple operational semantics for concurrent programs,and use foot-prints as a record of the memory addresses during execution.Conflicting foot-prints indicate conflicting accesses to memory.Then we define the notion of data-race-freedom operationally based on the preemptive operational semantics and footprints,which is the basis of our work.· We propose non-preemptive semantics for DRF programs.In addition to mem-ory accesses,our language allows externally observable operations such as I/O operations.Threads in the semantics can be preempted only at the end of each atomic block or after the I/O operations.And we find it unneccessary to allow preemption at the begining of each atomic block.· We define the semantics equivalence based on the set of execution traces in each semantics.Then we formally prove that our non-preemptive semantics is equiv-alent to the preemptive one for data-race-free programs,which is the main con-tribution of this thesis.·We also give a new operational notion of DRF in the non-preemptive semantics,which is called NPDRF.We prove that NPDRF is equivalent to the original defini-tion of DRF in the preemptive semantics.This allows one to study DRF programs fully within the non-preemptive semantics(and we may discard the preemptive execution).This thesis provides theorical basis for equivalence of preemptive and non-preemptive semantics.Our team has set up the verification of CASCompert,a complier from Clight to x86 for data-race-free concurrent programs,and the verification is based on the equiv-alence of preemptive and non-preemptive semantics.In fact,a great part of the verifi-cation is completed under non-preemptive semantics.