一种宽容的多线程程序内部时间信息流类型系统

摘要

提出了一种针对多线程程序的内部时间信息流的宽容的类型系统.在隐藏竞争变量集合的基础上定义了非干扰属性的形式化规范;在类型系统中区分了隐藏线程,细化了对内部时间信息流发生场景的分析.相对于已有的基于类型理论的方法,本类型系统可以允许更多实质上安全的代码通过类型检查.另外,类型系统的可靠性是在独立于调度模型的情况下证明的.