29 ноября 2011 г.

Puzzler из concurrency-interest

Замечательную штуку вчера продемонстрировал Hans Boehm в листе рассылки concurrency-interest (любопытно, что тема началась с запроса на легализацию разных трюков с s.m.Unsafe -- дискуссии concurrency-interest частенько очень сильно плутают). Ханс писал про опасность методов типа lock.tryLock() -- в смысле сложности их правильного понимания. Вот, например, код:

//Thread 1:
x = 17;
l.lock();

//Thread 2:
while ( l.tryLock() ) {
    l.unlock();
}
... x ...  // какое значение у x в этой точке?

Чтобы ответить на вопрос, обязан ли x быть равным 17 в конце второго потока надо ответить на вопрос "есть ли здесь data race?"

С одной стороны, с точки зрения "универсального" определения программа считается data race free если для всех sequentally consistent трасс над ней отсутствует конкурентный доступ к данным. В данном случае, кажется, это выполняется -- во всех SC трассах сначала в x пишется 17, и только потом x читается -- поэтому кажется, что код data race free, а значит после цикла во втором потоке x должен быть равен 17.

С другой стороны, JMM определяет data race free несколько иначе -- все конкурирующие доступы к данным должны быть упорядочены через happens-before. Поскольку между потоком 1 и 2 нет никаких ребер HB, то доступы к x на запись и на чтение в разных потоках не упорядочены через HB, и, следовательно, они образуют гонку -- а значит, значение x после цикла во втором потоке не определено.



Найти правильную точку зрения сравнительно просто -- достаточно вспомнить, что критические секции (и вообще, и в java в частности) имеют семантику "можно войти, нельзя выйти" (roach motel semantics) -- код может вноситься внутрь секции, но не может выноситься из нее. Это значит, что x=17 и l.lock() в потоке 1 могут быть переупорядочены -- присвоение может быть внесено в критическую секцию. Это сразу дает право сказать, что здесь таки есть гонка, и значение x во втором потоке действительно не определено.

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

А ошибка в рассуждениях в том, что, когда мы придумываем SC трассы над кодом, мы делаем два неявных предположения о том, что такое лок. Первое из них -- что лок неявно содержит некое состояние -- каким потоком он сейчас захвачен. Это состояние меняется вызовами lock()/unlock(), а так же запрашивается, и, возможно, меняется вызовом tryLock(). И это предположение верно -- у лока действительно есть это внутреннее состояние.

Но есть еще и второе предположение -- что изменения этого состояния методами lock()/unlock()/tryLock() -- имеют семантику volatile store/load. И вот это уже не верно. В соответствии со спецификацией, lock()/tryLock() имеют (==обязаны иметь) только семантику acquire, а unlock() -- только семантику release. А это значит, что мы не все трассы рассмотрели.

Путаницы добавляет тот факт, что на реализация блокировок обычно делается через CAS, а CAS на x86 имеет семантику full fence. То есть на x86 для любой реализации монитора (из мне известных) lock() будет иметь семантику full fence просто в силу того, что аппаратная модель памяти соответствующего процессора более слабых барьеров не предусматривает. И код Ханса будет скорее всего работать корректно (==не будет содержать гонок). Но это особенности именно аппаратной модели памяти конкретного процессора. Скажем, на пресловутых Azul-ах есть CAS без семантики барьера, и есть односторонние барьеры. И там вполне можно реализовать (правда, не на уровне java, а разве что на уровне интринсиков JIT-а) монитор, у которого lock() будет иметь честную семантику только acqiure.

Собственно, если я правильно понял Ханса, он и обращает внимание на то, что с введением методов типа tryLock() монитор становится легко принять за этакую неявную volatile переменную -- что не соответствует реальной семантике операций с мониторами.

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

  1. я правильно понимаю, что корень проблемы это CAS, который может завершиться отрицательно (т.е не смог захватить lock), что на некоторых платформах не пробивает барьер памяти ?
    но при этом успешны CAS - пробивает, или таки тоже нет?

    ОтветитьУдалить
  2. Да нет, корень проблемы -- если я правильно понял вопрос -- в том, что есть платформы, где CAS вообще не связан с барьером. И барьеры -- если они нужны -- приходится добавлять к CAS явно. И тогда можно реализовать захват блокировки как CAS+acquire fence. Такая реализация блокировки будет соответствовать контракту, но описанный код будет работать не так, как наивно ожидалось.

    ОтветитьУдалить
  3. т.е ключевой момент:
    есть платформы, где CAS вообще не связан с барьером

    (буду признателен за ссылки на тему).

    И второй момент - правильно ли, что текущие lock'и (н-р RL) работают CAS+acquite fence (я говорю не о x86 и подобных, а о azul в частности) ?

    ОтветитьУдалить
  4. Ну, собственно, Azul-ы -- главный известный мне пример. Клифф Клик об этом их свойстве часто упоминает в контексте своей реализации ConcurrentMap.

    Я не видел JDK для Azul-ов. Сильно сомневаюсь, что они переписывали стандартные классы под себя -- уж больно это чревато непредвиденными последствиями для переносимости. Более того, на текущий момент нет возможности реализовать Lock средствами джавы как fencelessCAS+acquire просто потому, что AtomicXXX.CAS -- имеет по контракту семантику full fence -- это раз. .weakCAS -- имеет не очень внятную семантику памяти -- два. И средств делать дифференциированные барьеры памяти в джаве пока нет -- три. Так что реализовать такое сейчас -- как я и писал -- можно только вводя специальные интринсики компилятора, расширяющие стандартные возможности. Сомневаюсь, что кто-то этим озадачился.

    ОтветитьУдалить
  5. >В соответствии со спецификацией, lock()/tryLock() имеют (==обязаны иметь) только семантику acquire

    Можно подробнее где требуется чтобы tryLock было обязано иметь семантику acquire? В JLS про это не говорится. В javadoc про это тоже не говорится.

    >>Но это особенности именно аппаратной модели памяти конкретного процессора
    Правильнее говорить "это особенность реализации ReentrantLock".

    Вот простой пример реализации ReentrantLock, который, очевидно, будет приводить к data race на tryLock, но тем не менее, будет удовлетворять javadoc'у для Lock:

    class MyLock ... {
    boolean islocked;
    volatile boolean islockedVolatile;

    public boolean tryLock() {
    if (islocked) return false; // optimization to avoid volatile access in hot path :)
    return islockedVolatile;
    }
    public void lock() {
    islocked=true;
    islockedVolatile=true;
    }

    При такой реализации метод tryLock может сработать вообще без volatile read, а значит будет типичный data-race.
    1-ый поток записал x=17, isLocked=true; Второй прочитал non-volatile isLocked==true, полез в x, и получил 0.
    Тут даже компилятор сможет переставить местами запись x=17 и isLocked=true.

    ОтветитьУдалить
    Ответы
    1. >Можно подробнее где требуется чтобы tryLock было обязано иметь семантику acquire?

      неудачный tryLock() не обязан иметь никакой memory semantics, это явно описано в Lock. Удачный имеет ту же семантику, что и lock(), очевидно.

      >от простой пример реализации ReentrantLock, который, очевидно, будет приводить к data race на tryLock, но тем не менее, будет удовлетворять javadoc'у для Lock:

      Это хороший пример для ситуации выше, да, но я сомневаюсь, что это корректная реализация: поскольку использование переменной islocked может происходить через data race, то ее значение простыми средствами не определено, может быть произвольным. Это значит, что вы можете получить tryLock() -> false _внутри_ уже захваченного лока. Что, очевидно, противоречит контракту RL. Другими словами, я не вижу как здесь можно доказать выполнения условия (tryLock() always return true if invoked inside lock()/unlock() region).

      Удалить