首页>
外国专利>
Method for Multithreaded Program Output Uniqueness Testing and Proof-Generation, Based on Program Constraint Construction
Method for Multithreaded Program Output Uniqueness Testing and Proof-Generation, Based on Program Constraint Construction
展开▼
机译：基于程序约束构造的多线程程序输出唯一性测试与证明的方法
展开▼
页面导航
摘要
著录项
相似文献
摘要
Provided is a method for multithreaded program output uniqueness testing and proof-generation, based on program constraint construction; according to multithreaded program semantics, a constraint expression is constructed; an output uniqueness verification problem is converted to a constraint solving problem; a constraint solver is used to detect the presence of different outputs, and a counterexample execution path describing different outputs is generated; first, a tested program is stubbed, and the program is executed to obtain an execution path; then, according to multithreaded program execution semantics, the execution path is converted to a first-order logic expression having no quantifiers, the constraint expression encompassing all possible thread interleavings; then, uniqueness verification conditions are constructed for the output of a first run; lastly, the constraint solver is used for verifying whether a path is causing the output value and the run result to be inconsistent. The present method detects whether the output of a multithreaded program is unique from a given input; if outputs are not unique, a counterexample sequence is displayed to describe the triggering process of same.
展开▼
