自动生成并发检查

本文介绍ATAB，一个为动作树自动生成成对可达性检查的工具。动作树可用于研究真实世界并发程序的行为。ATAB将成对可达性检查编码为交替树自动机，以判定一个动作树是否存在一种调度，使得程序中任意给定点对同时可达。由于成对可达性问题一般而言不可判定，ATAB在一种受限的基于锁的并发形式下工作。ATAB生成的交替树自动机比先前使用的那些更紧凑且可更高效检查。该过程完全自动化，简化了为更复杂动作树编码检查的过程。所生成的交替树自动机比以往的构造更易于扩展到大量锁。