模型检测：片上多核处理器核协调性验证研究的开题报告.docx

模型检测：片上多核处理器核协调性验证研究的开题报告
一、题目
片上多核处理器核协调性验证研究
二、研究背景和意义
随着系统集成度和处理器数量的不断提升，片上多核处理器（CMP）越来越受到人们的关注。CMP的性能与应用质量取决于多个处理器核之间的协调性，因此核协调性验证是重要的研究问题。
CMP涉及多个协同工作的处理器核，因此核协调性验证需要考虑以下方面：
（1）数据的正确性：处理器核之间传输的数据需确保正确性。
（2）时序的正确性：这与数据的正确性密切相关，需要确保所有处理器核的时序保持同步，否则会影响数据的正确传输。
（3）任务的正确性：多个处理器核之间需要协调完成某些复杂任务，需要验证任务执行的正确性。
（4）互斥和同步问题：处理器核之间的互斥和同步是保证多任务执行正确性的关键。
因此，CMP的核协调性验证是实现高性能和高质量应用的重要因素。
三、研究内容和方法
本研究将从数据的正确性、时序的正确性、任务的正确性和互斥同步问题等方面进行CMP的核协调性验证，并提出相应的验证方法。
1.数据的正确性
针对数据正确性问题，本研究提出两种验证方法：
（1）模型检测：使用模型检测方法验证CMP内数据传输的正确性，通过对验证模型进行性质验证，来发现可能导致数据传输错误的状态序列。
（2）仿真：使用仿真模拟不同的场景和应用，以检测数据传输中出现的错误。
2.时序的正确性
在保证数据正确性的前提下，需要确保所有处理器核的时序保持同步，从而避免出现数据同步方面的错误。为此，本研究将使用时序逻辑的形式化语言来描述和验证时序的正确性，以确保所有处理器核的时序保持同步。
3.任务的正确性
多个处理器核之间需要协调完成某些复杂任务，需要验证任务执行的正确性。本研究将使用形式化规范语言来描述任务过程和任务执行过程，以便对任务执行过程进行检查和验证。
4.互斥和同步问题
为确保CMP的高效执行，必须考虑处理器核之间的互斥和同步，以避免出现竞争和死锁。为此，本研究将采用Petri网模型来描述CMP内不同核之间的互斥和同步关系，然后进行形式化验证。
四、预期成果
本研究将设计并实现一套各方面都得到有效测试的核协调性验证工具。同时，将依据不同的场景，提供相关的用例和测试样例以及相应的评测和测试结果，有力地支持了CMP的性能和应用质量。
五、参考文献
[1]L.Li,M.Kandemir,I.Kolcu,J.H.Patel.Core-CoupledMemory:AFlexibleandEfficientMechanismforManagingMemoryHierarchiesinChipMultiprocessors.ACMTrans.Archit.CodeOptim.vol.8,no.2,pp.1-24,Jun.2012.
[2]R.Membarth,F.Hannig.SDF-MinMax:ADesignFlowFromDataflowProgramstoEfficientChipMultiprocessorExecution.IEEETrans.Comput.vol.62,no.12,pp.2455-2468,Dec.2013.
[3]J.Eom,S.Lee,J.Kim,Y.Kim,N.P.Jouppi,H.Kim.SIMD-SpecificOptimalCoreMappinginChipMultiprocessors.IEEETrans.Comput.vol.62,no.12,pp.2288-2301,Dec.2013.