收集合同和线程答案

【问题标题】：Collection Contracts and Threading收集合同和线程
【发布时间】：2010-10-06 16:10:01
【问题描述】：

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

    public void Add(T item)
    {
        _lock.EnterWriteLock();
        try
        {
            _items.Add(item);
        }
        finally
        {
            _lock.ExitWriteLock();
        }
    }

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

这里的基本问题是，只有在特定的锁定上下文中，并且只有在整个应用程序中一致地使用锁定来对集合的所有访问时，才能认为集合合同是有效的。我的集合必须从多个线程中使用（非冲突的添加和删除是一个有效的用例），但我仍然想实现ICollection<T>。我是否应该简单地假装我可以通过假设满足这个确保要求，即使我知道我不能？令我震惊的是，没有一个 BCL 集合实际上也可以确保这一点。

编辑：

根据进一步的调查，听起来最大的问题是合约重写器可能会引入不正确的断言，从而导致运行时失败。基于此，我认为我唯一的选择是将我的接口实现限制为IEnumerable<T>，因为ICollection<T> 上的合同意味着实现类不能提供内部线程同步（访问必须始终在外部同步。）这是可以接受的我的特殊情况（所有希望改变集合的客户都直接知道类类型），但我很想知道是否有其他解决方案。

【问题讨论】：

如果您使用假设，您可能仍然会遇到运行时合约错误。

标签： c# static-analysis code-contracts

【解决方案1】：

正如您所暗示的，没有实施者可以履行此合同。确实一般在面对多线程时，除非合约可以像这样应用：

 Take Lock
 gather Old Stuff

 work

 check Contract, which may compare Old Stuff
 Release Lock

我不明白如何履行任何合同。据我所知here 这是一个尚未完全成熟的区域。

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

【讨论】：

另一个想法：如果合约重写器为 Ensures 条件引入断言，这意味着断言在多线程使用下可能会失败...
这似乎在我给出的参考文献中得到承认。对我来说，这份合同看起来像是一个不错的主意，但还没有准备好迎接黄金时段。
想多了，我觉得这可能是合理的。合同断言基本上表明实现接口的类不是线程安全的，而且奇怪的是，您实际上违反了合同，试图在集合级别提供内部线程安全.我注意到 .NET 4 中的新并发集合没有实现 ICollection<T>。
目前几乎所有的接口合约都假设单线程访问。很难想象合约在多线程场景中如何工作。我认为基本上你在这里需要的是能够指定 when 应该检查后置条件 - 正如这篇文章所说:)

【解决方案2】：

using System.Diagnostics.Contracts;

namespace ConsoleApplication1
{
    class Class1
    {
        public int numberOfAdds    { get; private set; }
        public int numberOfRemoves { get; private set; }
        public int Count
        {
            get
            {
                return numberOfAdds - numberOfRemoves;
            }
        }

        public void Add()
        {
            Contract.Ensures(numberOfAdds == Contract.OldValue(numberOfAdds) + 1);
        }

        public void Remove()
        {
            Contract.Requires(Count >= 1);
            Contract.Ensures(numberOfRemoves == Contract.OldValue(numberOfRemoves) + 1);
        }

        [ContractInvariantMethod]
        void inv()
        {
            Contract.Invariant(Contract.Result<int>() == numberOfAdds - numberOfRemoves);
        }
    }
}

警告：不要使用大于小于比较；计数会溢出，但这些合约应该在这种情况下有效。使用像 int8 这样的小整数类型进行测试。确保使用不会引发溢出的整数类型。

【讨论】：