среда, 3 февраля 2016 г.

Асинхронные постусловия в библиотеке Code Contracts

На прошлой неделе я выкатил релиз-кандидат новой версии библиотеки Code Contracts (v.1.10-rc1). В этом релизе было поправлено довольно много, а главной «новой» возможностью стала вменяемая реализация асинхронных постусловий.

Для начала стоит напомнить, что такое постусловия вообще, и асинхронные постусловия в частности.

Постусловие метода – это некоторое условие, которое должно быть истинным при успешном завершении метода. Например, постусловие может гарантировать, что возвращаемое значение не будет равно null, что перед завершением метода Start, состояние будет равняться определенному значению (например, Starting) и т.п.

Вот небольшой пример:

public string GetResult()
{
   
Contract.Ensures(Contract.Result<string>() != null
);
   
return string.
Empty;
}

enum Status { Init, Starting, Started }
private Status
_status;

public void
Start()
{
   
Contract.Ensures(_status == Status.Starting);
}

(Обратите внимание, что в отличие от предусловий, постусловия могут ссылаться на закрытое состояние. Это связано с тем, что клиент класса не должен иметь возможности проверить валидность постусловия, это забота самого метода, ну и инструментов, вроде Code Contracts, которые вставляют проверку условий в каждой точке выхода из метода.)

Обычные предусловия предусловия имеют довольно ограниченную применимость в случае асинхронных методов. В случае метода, который возвращает Task или Task<T>, помимо проверки некоторое условия при выходе из методы, бывает очень полезным проверить некоторое условие во время завершения возвращаемой задачи. Именно для этих целей используются «асинхронные постусловия»).

ПРИМЕЧАНИЕ
Обратите внимание, что «асинхронные постусловия» применимы не только к методам, помеченным ключевым словом async, но и к любым методам, которые возвращают Task или Task<T>. Т.е. асинхронные методы применимы к любым методам, которые следуют TAP (Task-based Asynchronous Pattern)!

Давайте посмотрим на пример асинхронного постусловия. В случае асинхронного метода StartAsync, мы можем определить следующие правила:

· После окончания «синхронной» части метода StartAsync мы хотим гарантировать, что состояние будет равно Starting,

· А после окончания асинхронной операции (т.е. после завершения задачи), состояние должно быть Started.

Сделать это можно следующим образом:

private static Status _status = Status.Init;

public static async Task<Status
> StartAsync()
{
   
Contract.Ensures(_status == Status.
Starting);
   
// Или же можно использовать
    // Contract.Result<Task<Status>>().Result == Status.Started
    Contract.Ensures(Contract.Result<Status>() == Status.
Started);
   
// Если мы сделаем await до установки состояния в Staring,
    // то постусловие будет нарушено и мы получим ContractException
    _status = Status.
Starting;
   
await Task.Delay(42
);
    _status
= Status.
Started;
   
return _status;
}

Каждый раз, когда ccrewrite встречает в постусловии Contract.Result<T>() или Contract.Result<Task<T>>().Result, то он генерирует следующий код:

private class AsyncClosure
{
   
public Task<Status> CheckPost(Task<Status
> task)
    {
       
if (task.Status == TaskStatus.
RanToCompletion)
        {
           
__ContractRuntime.Ensures(task.Result == Status.
Started);
        }
       
return
task;
    }
}


public static Task<Status
> StartAsyncRewritten()
{
   
var asyncClosure = new AsyncClosure
();

    _status
= Status.
Starting;

   
// Проверка синхронного постусловия
    __ContractRuntime.Ensures(_status == Status.
Starting);

   
// Здесь генерируется таска с помощью асинхронного конечного автомата
    // и всяческих AsyncMethodBuilder-ов. Нам в данном случае это не интересно!
    Task<Status> task = null
;

   
// Проверка асинхронного постусловия с помощью продолжения
    return task.ContinueWith(asyncClosure.
CheckPost,
       
TaskContinuationOptions.ExecuteSynchronously).Unwrap<Status>();
}

В случае асинхронных постусловий, ccrewrite генерирует замыкание (класс AsyncClosure), с единственным методом CheckPost, который предназначен для проверки состояния по завершения задачи. (Да, в случае «исключительных» постусловий, т.е. постусловий, которые должны быть выполнены при генерации методом исключения, генерируется очень похожий код, просто проверка осуществляется только в случае, когда завершенная задача завершилась с ошибкой).

Идея реализации состоит в том, что постусловие проверяется в продолжении, которое задается с помощью ContinueWith на задаче, исходно возвращаемой из текущего метода. ContinueWith в этом случае, по сути декорирует исходную задачу и возвращает тот же самый результат, но с генерацией исключения в случае нарушения постусловия. Поскольку метод CheckPost возвращает Task<Status>, то возвращаемое значение метода ContinueWith будет Task<Task<Status>>. Это значит нам нужно воспользоваться трюком метода TaskExtensions.Unwrap и распаковать полученное значение для получения просто Task<Status>.

Теперь, если постусловие будет нарушено, то клиент получит ContractException, а если нет, то он получит исходную задачу, полученную в результате работы асинхронного метода.

ПРИМЕЧАНИЕ
Асинхронные постусловия были полностью переписаны в версии 1.10. Предыдущая версия генерировала совершенно другой код, который приводил к побочным эффектам, когда задача завершалась неудачно! Так что если у вас были проблемы с асинхронными в старых версиях Code Contracts, то не удивляйтесь – там они были реализованы очень криво!

Асинхронные постусловия не имеют особой синтаксической конструкции в библиотеке Code Contracts. Для их использования нужно в постусловии обратиться к свойству Result возвращаемой задачи, или же просто использовать Contract.Result<T>() в случае если метод возвращает Task<T>. Зная это можно сделать небольшой вспомогательный метод, который будет выражать намерения более явным образом, что может быть полезным, когда асинхронное постусловие должно проверять некоторое состояние объекта, и вообще не трогать возвращаемую задачу:

ПРИМЕЧАНИЕ
Да, асинхронные постусловия совершенно невозможно выразить, если метод возвращает Task!

public static async Task<int> StartAsync()
{
   
// Синхронное постусловие
    Contract.Ensures(_status == Status.
Starting);
   
// Асинхронное постусловие
    Contract.Ensures(AsyncPostcondition(_status == Status.Started, Contract.Result<int
>()));

    _status
= Status.
Starting;
   
await Task.Delay(42
);

    _status
= Status.
Started;
   
return 42
;
}

[
Pure]
private static bool AsyncPostcondition<T>(bool predicate, T
methodResult)
{
   
return predicate;
}
Дополнительные ссылки

18 комментариев:

  1. Сергей, к сожалению, постусловие которое ты пометил как "// Синхронное постусловие", без комментария будет вводить в заблуждение читателя кода. Ведь какая основная идея async методов? Чтобы такой метод выглядел синхронным и выполнял свои операторы последовательно (за исключением явного бранчевания вызовом нескольких асинхронных методов без await на каждом). Идея постусловия вроде как говорит, что оно будет проверено по завершению метода. Причем, в случае асинхронного метода лично я, как и, предположительно, многие, будут понимать именно _логическое_ завершение метода - ведь компилятор абстрагирует меня от _реальных_ деталей реализации (таких как возврат из метода на каждом await). Но в реальности выходит, что синхронное постусловие будет завязано на детали реализации async/await, и будет проверяться перед каждым await (почти предусловие). На мой взгляд, это делает такие постусловия бесполезными, а значит, сильно сужает полезность контрактов в классах, которые содержат много async методов (а на сегодняшний день такие классы составляют, на мой взгляд, не менее половины кода во многих проектах). Что мешает сделать синхронные постусловия ведущими себя асинхронно в асинхронных методах?

    ОтветитьУдалить
    Ответы
    1. Андрей, тут есть несколько важных моментов:

      1. Асинхронные постусловия применимы к любым TAP-методам, а не только к методам, помеченным ключевым словом async
      2. Асинхронный метод (помеченный ключевым словом async) таки содержит синхронную часть, которая будет выполняться до первого await-а и синхронное постусловие будет выполнено именно по окончанию синхронной части, *а не перед выходом из каждого await-а!*.

      Т.е. асинхронные/синхронные постусловия, ИМХО, ведут себя именно так, как ты бы хотел, а не так, как ты описал в комментарии:))

      Удалить
    2. Сергей, возможно я плохо формулирую проблему. Попробую короче: я ожидаю, что "синхронное" постусловие будет выполняться после _логического_ окончания метода (перед "return 42"), будь он синхронный или асинхронный. Проще говоря, лично я не делил бы постусловия на "синхронные" и "асинхронные". Контракты нацелены на проверку работы метода как юнита, т.е. я не знаю зачем мне промежуточная валидация состояния класса на момент выполнения await - ведь метод на этот момент еще далек от завершения своей задачи.

      Удалить
    3. Добавлю еще чтобы понять моих тараканов: Если я смотрю на асинхронный метод (тот, что с асинк), я как бы Task в возвращаемом значении не вижу, для меня он становится инфраструктурной штукой, которую вообще можно было бы не писать явно, если бы так решили дизайнеры языка (об этом кстати Joe Duffy интересно раасуждал в контексте Midori). Т.е. в таком методе его логическое завершение наступает тогда, когда таск получает значение с помощью return или ошибку с помощью исключения. С другой стороны, если метод не асинк, но таск он возвращает, я тогда интерпретирую именно таск как логический результат его работы, а не то, что этот таск произведет в конечном счете. В первом случае постусловие логично всегда проверять по завершению таска, во втором случае - по возврату таска или исключению.

      Удалить
    4. Вот пример на основе твоего кода как бы я хотел что бы в идеале выглядели контракты для асинхронных методов:

      public static async Task StartAsync()
      {
      // Я ожидаю в качестве конечного результата
      // запуск (чего бы то ни было) с соответствующим
      // статусом в поле _status после логического
      // завершения метода - т.е. после завершения таска.
      Contract.Ensures(_status == Status.Started);

      // Также, я ожидаю что, условно, время на запуск
      // было >= 0. Опять же, после завершения таска
      // (как я понял, уже необязательно писать
      // Contract.Result>().Result чтобы было
      // понятно, что меня интересует не сам таск, а
      // результат метода. Примерно такого же
      // "понимания" я жду и в случае первого постусловия.
      Contract.Ensures(Contract.Result() >= 0);

      // Здесь не ясно для кого выставляется
      // промежуточный статус. Асинхронный метод не
      // означает потокобезопасность - т.е. по умолчанию
      // пока метод выполняется асинхронно, никто не должен
      // обращаться к статусу "снаружи" (прямо или косвенно).
      // Ни постусловие, ни инвариант тут не применимы,
      // так как мы в середине метода.
      // Если же асинхронный вызов, который идет далее,
      // ожидает такой смены статуса (если он тоже метод
      // этого класса), это может быть причиной,
      // но в качестве контракта я бы поставил Assert
      // (представим, что статус меняется более сложным кодом).
      // В любом случае, я бы избегал промежуточных
      // состояний, которые, в случае исключения, могут
      // оставить класс в некорректном состоянии.
      _status = Status.Starting;

      Contract.Assert(_status == Status.Starting);

      // Делаем много работы, метод далек от завершения.
      // Нет причин проверять какое-либо постусловие.
      await Task.Delay(42);

      // Делаем еще больше работы.
      // Первым делом, первым делом работа, ПОСТусловия - потом :)
      await Task.Delay(84);

      // Сделано!
      _status = Status.Started;
      int timeElapsed = 42 + 84;

      // Теперь пора проверить, что статус Started и
      // что время не отрицательное.
      return timeElapsed;
      }

      Удалить
    5. Сорри, там в коде повырезались кусочки с угловыми скобками, фильтруют HTML :)

      Удалить
    6. Андрей, мне кажется, нам нужно разделить дискуссию на то, что есть сейчас и на то, что мы бы хотели видеть в будущем в идеальном языке.

      Я описывал то, что есть сейчас и как текущие возможности можно использовать для проверки разных штук. Я ж не разрабатываю новые контракты или новый язык программирования:)

      Именно поэтому я разделил синхронные и асинхронные постусловия. С моей точки зрения - это наиболее простой способ понять, как же будет вести себя переписанный код и каких гарантий можно добавиться с помощью существующего инструмента.

      Удалить
    7. Да, ты прав, я немного помечтал. С другой стороны, это все-таки фидбек :)

      Удалить
    8. Андрей, фидбек не просто валидный, он очень и очень полезный:)) Есть даже мысли, когда его применить;)

      Удалить
    9. Спасибо, буду ждать :)

      Удалить
  2. В продолжение: в приведенном коде ты вроде как с пользой применил синхронное постусловие чтобы проверить статус перед асинхронным вызовом (хотя, опять же, я не чувствую, что это постусловие, скорее assert):
    Contract.Ensures(_status == Status.Starting);
    Это будет хорошо работать, пока ты не добавишь еще один асинхронный вызов (после _status = Status.Started). Как я догадываюсь, асинхронное постусловие проверится и перед ним тоже, и там оно уже будет невалидное (ведь статус уже НЕ Starting). Получается довольно специфический случай, когда синхронное постусловие будет работать.

    ОтветитьУдалить
    Ответы
    1. Как я написал к предыдущему комментарию, синхронные постусловия никак не завязаны на количество await-ов, а проверяются лишь раз - по завершению синхронной части метода:).

      > Как я догадываюсь, асинхронное постусловие проверится и перед ним тоже, и там оно уже будет невалидное (ведь статус уже НЕ Starting).
      Есть смысл просто проверить самому:))

      З.Ы. Напомню, что code contracts - это тула, которая работает на уровне IL-а, а значит "рассахарить" асинхронный метод для нее будет очень и очень сложно. Особенно в свете изменений, которые внес Roslyn;)

      Удалить
    2. Понимаю насчет трудностей реализации. Как компромисс между текущей реализацией и встраиванием контрактов в язык MS могла бы предоставить в компилере возможность инжектить что-то типа пролога и эпилога для методов (поклонники AOP были бы рады). К примеру, компилятор сам знает где у метода точки завершения, включая асинхронные со всеми сложностями. Далее, если компилятор видит в методе вызов другого метода, и этот метод каким-то способом (атрибутом?) называет себя эпилогом, компилятор встраивает вызов этого метода во все места, где метод логически завершается. Условно говоря, если таким методом является Contract.Ensures, он мог бы делегировать проверку контракта своему рантайму без всякого переписывания IL и без риска что-то упустить.

      Удалить
    3. Насчет второго вызова я неправ, согласен, так как на каждый await по сути отдельный вход в метод, то и проверка постусловия каждый раз одна - перед очередным await.

      Удалить
    4. У нас были дискуссии с разработчиками компилятора по поводу предложенной тобой точки расширения, но эти разговоры ничего не дали. Никто не хочет давать такую возможность, которая может все сломать:(

      Удалить
    5. А как быть, если ты заранее не знаешь, закончится метод синхронно или асинхронно? Ну, например, у тебя там кэширование прописано, и если функция находит результат в кэше - синхронно его возвращает, если не находит - делает асинхронный вызов к какому-то сервису. Как тогда написать пост-условие, если у нас в половине случаев sync==async, а в другой половине все наоборот?

      Удалить
  3. А что насчет инвариантов? CC начнет проверку инварианта только после завершения Task'и или до await и после? И еще вопрос: как разрешается такой сценарий: запускаются две задачи, которые меняют состояние класса, одна задача уже разрешилась, но инвариант еще не проверен, а другая задача только выполняется, но во время выполнения нарушается инвариант класса (что легально), то во время проверки инварианта в первой задаче произойдет исключение. Такой сценарий можно разрешить самому обычной синхронизацией на уровне инварианта или это может разрешить сам CC?

    ОтветитьУдалить
    Ответы
    1. ИМХО, инварианты с асинхронными методами работать нормально не будут. Такого понятия, как асинхронного инварианта не существует, а значит, они будут проверяться по завершению синхронной части методов (в случае методов с async - до первой встречи с await-ом).

      > И еще вопрос: как разрешается такой сценарий: запускаются две задачи, которые меняют состояние класса, одна задача уже разрешилась, но инвариант еще не проверен, а другая задача только выполняется, но во время выполнения нарушается инвариант класса (что легально), то во время проверки инварианта в первой задаче произойдет исключение.
      Никак. Инвариант нельзя выразить для асинхронных методов..

      Удалить