Liveness of Concurrent Program

验证liveness属性会比safety更难，而且对并发程序而言，一般需要对调度器(scheduler)的公平性进行假定。