当涉及锁定时,代码合同警告"确保未经证实"

Question

我正在尝试lock使用以下示例来研究.NET Code Contracts如何与关键字进行交互:

public class TestClass
{
  private object o1 = new object();
  private object o2 = new object();

  private void Test()
  {
    Contract.Requires(this.o1 != null);
    Contract.Requires(this.o2 != null);
    Contract.Ensures(this.o1 != null);

    lock (this.o2) {
      this.o1 = new object();
    }
  }
}

当我运行代码契约静态分析工具时,它会打印一个警告: Ensures unproven: this.o1 != null

如果我做了以下任何一项:

• 改变o2在lock给o1,
• o1将lock块内部更改为o2,
• 在lock块内添加第二行,分配new object给o2
• 更改lock (this.o2)到if (this.o2 != null),
• lock完全删除声明.

警告消失了.

但是,将lock块内的行更改为var temp = new object();(从而删除方法中的所有引用o1)仍会导致警告:

private void Test()
  {
    Contract.Requires(this.o1 != null);
    Contract.Requires(this.o2 != null);
    Contract.Ensures(this.o1 != null);

    lock (this.o2) {
      var temp = new object();
    }
  }

---

所以有两个问题:

1. 为什么会出现此警告？
2. 可以采取哪些措施来防止它(请记住这是一个玩具示例,lock实际代码中实际发生了什么事情)？

Answer 1

以下是静态检查器处理锁和不变量的方式：

如果您使用 lock(x.foo) { ... } 形式锁定某些内容，则静态检查器会将 x.foo 视为 x 的保护锁。在锁作用域的末尾，它假设其他线程可能访问 x 并修改它。结果，静态检查器假设 x 的所有字段仅满足锁定范围之后的对象不变式，仅此而已。

请注意，这并没有考虑所有线程交错，只是考虑锁范围末尾的交错。