Кодовые контракты предупреждают о недоказанных гарантиях при использовании блокировок

Я пытаюсь понять, как контракты кода .NET взаимодействуют с ключевым словом lock, используя следующий пример:

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();
    }
  }
}

Когда я запускаю инструмент статического анализа Code Contract, он выводит предупреждение: 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 в реальном коде что-то происходит)?

.net c# code-contracts
person Philip C    schedule 22.04.2013    source источник
comment
По-видимому, Code Contracts не считает создание экземпляра o1, которое происходит автоматически во время выполнения конструктора, достаточным доказательством, гарантирующим o1!=null. Гарантия — это постусловие, а lock означает, что метод будет вызываться из нескольких потоков.   -  person Robert Harvey    schedule 22.04.2013
comment
@RobertHarvey Но, как я уже сказал, если вы измените this.o1 = new object() на this.o2 = new object(), все в порядке. В этом случае он не может гарантировать ничего, чего нельзя было бы гарантировать в исходном случае, и он по-прежнему включает блокировку. И Requires должно быть достаточным доказательством того, что o1 не равно нулю в начале метода.   -  person Philip C    schedule 23.04.2013

Ответы (2)


arrow_upward
2
arrow_downward

Вот как статическая проверка обрабатывает блокировки и инварианты:

Если вы заблокируете что-либо с помощью формы lock(x.foo) { ... }, программа статической проверки будет рассматривать x.foo как защитную блокировку x. В конце области блокировки предполагается, что другие потоки могут получить доступ к x и изменить его. В результате статическая проверка предполагает, что все поля x удовлетворяют только инварианту объекта после области блокировки, не более того.

Обратите внимание, что здесь не учитываются все чередования потоков, а только чередования в конце областей блокировки.

person Manuel Fahndrich    schedule 24.04.2013

arrow_upward
1
arrow_downward

Добавьте в свой класс следующий код:

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(o1 != null);
    }

Я не могу сказать вам, почему, но в этом случае статический верификатор, по-видимому, рассматривает приватное назначение поля и отсутствие методов, которые его изменяют, как достаточное доказательство того, что поле не будет изменено. Это может быть ошибка в верификаторе? Возможно, стоит сообщить об этом на форуме Code Contracts.

person Stephen J. Anderson    schedule 24.04.2013
comment
Я вижу, как это исправит ситуацию, но в моем реальном классе это на самом деле не инвариант — он просто всегда истинен до вызова этого метода, и метод не меняет этого факта. - person Philip C; 24.04.2013