Universes for Race Safety
Universes for Race Safety
复制标题
赛车安全宇宙
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
S. Drossopoulou
中科院分区：
文献类型：
--
作者：
D. Cunningham;S. Eisenbach;S. Drossopoulou
当两个错误的同步线程访问相同的对象时，就会发生种族条件。守卫在访问对象的关系之前已被锁定。简单的所有权类型。证明在执行正确的程序期间，我们支持竞赛条件。妥协使用此类对象的所有权域的同步策略是完全知道的，我们开发了一种使用效果来处理未知所有权域对象的非结构（即可变）途径的新技术。
Race conditions occur when two incorrectly synchronised threads simultaneously access the same object. Static type systems have been suggested to prevent them. Typically, they use annotations to determine the relationship between an object and its “guard” (another object), and to guarantee that the guard has been locked before the object is accessed. The object-guard relationship thus forms a tree similar to an ownership type hierarchy. Universe types are a simple form of ownership types. We explore the use of universe types for static identification of race conditions. We use a small, Java-like language with universe types and concurrency primitives. We give a type system that enforces synchronisation for all object accesses, and prove that race conditions cannot occur during execution of a type correct program. We support references to objects whose ownership domain is unknown. Unlike previous work, we do so without compromising the synchronisation strategy used where the ownership domain of such objects is fully known. We develop a novel technique for dealing with non-final (i.e. mutable) paths to objects of unknown ownership domain using effects.