A Multithread-oriented Compiling Verification Model

Nowadays,as the scale of software expanding largely,how to ensure the execution of software keep the consistency of expectation can be a big problem to all software developers and researchers.Since compiler has a special position in the computer software system,it is regarded as a critical part in guarantee the correct execution of software programs.Ensure the credibility of compiler generally adopt formal verification method--proving the semantic equivalence of source language program and target language program on the basis of the formal definition of the source language,target language and the compilation process.In this paper,according to the characteristics of the Java language,we proposes a compile validation model which supports multithreading.Concrete research content is as follows:First,defining Jmin,a language that is suitable for prove,and formalized definition of its semantic.Jmin language is a subset of the Java language,support for the core of Java syntax:it is object-oriented,can throw and handle exceptions and perform some threads operations.This paper also define Jmin virtual machine model and its instruction set based on Java virtual machine instructions.Second,formally describes the compilation process,and the use of theorem proving tools Isabelle/HOL to prove the validity of the compilation process.Third,on the basis of correctness proof,Jmin trusted compiler implementation framework is given.