收集合同和线程

Dan*_*ant 9 c# static-analysis code-contracts

假设我有一个自定义集合类,它提供了一些内部线程同步.例如,简化的Add方法可能如下所示:

    public void Add(T item)
    {
        _lock.EnterWriteLock();
        try
        {
            _items.Add(item);
        }
        finally
        {
            _lock.ExitWriteLock();
        }
    }
Run Code Online (Sandbox Code Playgroud)

最新的Code Contracts抱怨说CodeContracts: ensures unproven: this.Count >= Contract.OldValue(this.Count).问题是这真的无法证明.我可以确保在内部锁定内,Count将大于其先前的值.但是,在方法的退出处,我无法确保这一点.退出锁之后,在方法完成之前,另一个线程可以发出两个Removes(可能是不同的元素),使合同无效.

这里的基本问题是,只有在整个应用程序中一致地使用锁定以对集合进行所有访问时,才能认为集合合同在特定锁定上下文中是有效的.我的集合必须在多个线程中使用(非冲突的Add和Remove是一个有效的用例),但我仍然希望实现ICollection<T>.即使我知道我不能,我是否应该假装我能够满足这个确保要求的假设?令我印象深刻的是,BCL系列中没有一个能够真正确保这一点.


编辑:

基于一些进一步的调查,听起来最大的问题是合同重写者可能引入不正确的断言,导致运行时失败.基于此,我认为我唯一的选择是限制我的接口实现IEnumerable<T>,因为合同ICollection<T>暗示实现类不能提供内部线程同步(访问必须始终在外部同步.)这对我的特定情况是可接受的(所有客户端)希望改变集合直接了解类类型,但我很想知道是否有其他解决方案.

djn*_*jna 2

正如您所暗示的,没有实施者可以履行该合同。事实上,通常面对多线程,除非契约可以像这样应用:

 Take Lock
 gather Old Stuff

 work

 check Contract, which may compare Old Stuff
 Release Lock
Run Code Online (Sandbox Code Playgroud)

我不明白如何履行任何合同。从我这里可以看到,这是一个尚未完全烘烤的区域。

我认为使用 Assume 是你能做的最好的事情,实际上你是在说“通过调用 Add 我正在做合同期望的事情”。