Research On Verification Of The Multi-core Processor Memory Systems

Research on Verification of theMulti-core Processor Memory SystemsThe multi-core and many-core processors have become the mainstreamprocessor architecture.Processors have evolved from single-core to multi-core (many-core) processor, the memory system changes the most significant.These changes constitute a new challenge to the verification work of the memory systems of multi-core processors. We carried out research work in the multi-core processor memory system verification. The main content of the thesis is the verification of cache coherence protocols and memory consistency model validation. We have made some progress in Intel MESIF protocol formalized modeling and model checking, and fast memory consistency model validation methods and tools.There are three main areas in the creative work of this thesis:(1) We analyze for Intel Nehalem micro-structure MESIF Cache coherenceprotocoland formal model the protocol by the SMV formal language.We use NuSMV tool to verify the protocol, the tool generates a counterexample. By counterexample analysis, we refined the protocol. The difficulty of Cache coherence protocol is the verification of the parameterized protocol. We use PaTLV toolto verify the parameterized MESIF protocol. This is a useful attempt to useparameterized model checking methods in industrial Cache coherence protocol verification.(2) We propose a fast dynamic verification approach of memory consistency model. We take advantage of multi-core processor systems performance counters to get the criticalinformation of activememory access instruction set by periodically scanning performance counters.On this basis, it is possible to obtain a naturallytimesequence relationship between the sets of instructions. In the time sequence constraints, memory consistency model validation can be localized, and memory consistency verification time complexity is greatly reduced.(3) We have implemented a general purpose memory consistency model validation tool MOTEC+.The MOTEC+tool can verify many memory consistency models, including: sequential consistency model, processor consistency model, and release consistency model. Experimental results show that the MOTEC+toolcan quickly verify memory consistency model.