上科大逻辑与形式化验证讲座2

讲的是GPU kernel的形式化验证。

大概意思就是形式化生成工具利用kernel给出的漏洞，生成barrier。由于gpu会有很多的并发程序，导致data race ，在cpu中有死锁机制，而gpu就是barrier。

原子化步骤的概念还是很清晰的。这个概念真的和量子纠缠很有关系，就是一个黑盒，只知道原子步骤的