约束求解问题
给定一组约束,求:
- 这组约束是否可满足
- (可选)如果可满足,给出一组赋值
- (可选)如果不可满足,给出一个较小的矛盾集 unsatisfiable core
总的来说是不可判定的问题,但存在很多可判定的子问题:
如:
给定一组约束,求:
总的来说是不可判定的问题,但存在很多可判定的子问题:
如:
摘要
由于线程交错的数量很大,分析多线程程序是困难的。偏序关系可用于建模和分析多线程程序。然而,目前尚无专用的决策过程用于解决偏序约束。在本文中,我们提出了一种新颖的有序一致性理论,用于在顺序一致性下验证多线程程序,并详细阐述了其理论求解器。该求解器实现了增量一致性检查、最小冲突子句生成和专用理论传播,以提高 SMT 求解的效率。我们在可信赖的基准测试上进行了大量实验,结果显示我们的方法显著提升了性能。
作者:清华大学软件学院 贺飞、Zhihang Sun、Hongyu Fan
现在的计算系统中普遍使用共享内存多线程程序。并发程序的交错数量使得其在实践中很难进行验证。因此,开发技术来缓解并发程序验证中的执行爆炸问题是非常有意义的。
使用模式的最佳方式之一是让他们走出家门,这样他们就可以与其他模式互动。 你使用模式越多,你就会越多地看到它们一起出现在你的设计中。对于在设计中协同工作的一组模式,可以应用于许多问题,我们有一个特殊的名称:复合模式(Compound Pattern)。没错,我们现在说的是模式的模式!
1 |
|
方案 1 | 方案 2 |
---|---|
![]() |
![]() |