Хабр Курсы для всех
РЕКЛАМА
Большая витрина: от крупнейших школ до частных авторов. Сравнивайте по цене, длительности, формату и выбирайте самый подходящий курс!
Хабр доступен 24/7 благодаря поддержке друзей
Комментарии 8
>Применение более слабых моделей – acquire/release или relaxed – требует верификации алгоритма.
Тут очень двусмысленно звучит — как будто, если вы используете SC-модель доступа к атомикам, то верификация вообще не нужна. Даже если мы говорим только про отсутствие data race (а не про race conditions) — SC-семантика гарантирует вам data race free только и именно для тех переменных, к которым вы обращаетесь через SC-примитивы. Для всех остальных переменных ничего априори не гарантируется, все гарантии необходимо выводить через те самые happens-before, за которыми вы послали так далеко :). А ведь ни одна разумная программа не состоит только из атомиков, так что даже используя только SC-атомики можно легко и непринужденно получить код с гонками за счет «обычных» переменных, которые не несут явной спецификации memory-order. Мне кажется, это ваше утверждение стоит уточнить, во избежание
Тут очень двусмысленно звучит — как будто, если вы используете SC-модель доступа к атомикам, то верификация вообще не нужна. Даже если мы говорим только про отсутствие data race (а не про race conditions) — SC-семантика гарантирует вам data race free только и именно для тех переменных, к которым вы обращаетесь через SC-примитивы. Для всех остальных переменных ничего априори не гарантируется, все гарантии необходимо выводить через те самые happens-before, за которыми вы послали так далеко :). А ведь ни одна разумная программа не состоит только из атомиков, так что даже используя только SC-атомики можно легко и непринужденно получить код с гонками за счет «обычных» переменных, которые не несут явной спецификации memory-order. Мне кажется, это ваше утверждение стоит уточнить, во избежание
Согласен, во фразе, наверное, не хватает "особо требует верификации".
Про data race — тоже согласен. По сути, обращение к атомарной переменной — это всегда data race; можно сказать, что это легализованный стандартом data race, все остальные — UB.
Про отношения happend-before и пр. Подготавливая эту заметку, я метался между подходом C++11 (отношениями) и тем, из чего вырос этот подход — барьерами. Не умаляя достоинств отношений и аксиоматики, хочу сказать, что всё же более приземленный подход, основанный на постановке барьеров, мне импонирует больше, он для меня более понятен и более применим. Барьер я могу пощупать, он материален, он воплощается в инструкции процессора. Об отношениях пусть говорят люди более сведущие, например, А.Вильямс.
Я не видел работ, объясняющих расстановку memory ordering с точки зрения happens-before и прочих в чем-то более сложном, чем стек или самая простая очередь. Да, существует ряд исследований, посвященных попыткам автоматизации расстановки memory ordering в алгоритмах (насколько помню, Dechev и другие), но серьезных успехов к настоящему времени не достигнуто, насколько я знаю.
Мне кажется, что для модели памяти C++11 не хватает типичных паттернов применения. По моим наблюдениям, такие паттерны все-таки существуют, по крайней мере в алгоритмах lock-free структур данных, но пока не нашлась пресловутая «банда четырех» для их обнаружения и «легализации».
Про data race — тоже согласен. По сути, обращение к атомарной переменной — это всегда data race; можно сказать, что это легализованный стандартом data race, все остальные — UB.
Про отношения happend-before и пр. Подготавливая эту заметку, я метался между подходом C++11 (отношениями) и тем, из чего вырос этот подход — барьерами. Не умаляя достоинств отношений и аксиоматики, хочу сказать, что всё же более приземленный подход, основанный на постановке барьеров, мне импонирует больше, он для меня более понятен и более применим. Барьер я могу пощупать, он материален, он воплощается в инструкции процессора. Об отношениях пусть говорят люди более сведущие, например, А.Вильямс.
Я не видел работ, объясняющих расстановку memory ordering с точки зрения happens-before и прочих в чем-то более сложном, чем стек или самая простая очередь. Да, существует ряд исследований, посвященных попыткам автоматизации расстановки memory ordering в алгоритмах (насколько помню, Dechev и другие), но серьезных успехов к настоящему времени не достигнуто, насколько я знаю.
Мне кажется, что для модели памяти C++11 не хватает типичных паттернов применения. По моим наблюдениям, такие паттерны все-таки существуют, по крайней мере в алгоритмах lock-free структур данных, но пока не нашлась пресловутая «банда четырех» для их обнаружения и «легализации».
>По сути, обращение к атомарной переменной — это всегда data race; можно сказать, что это легализованный стандартом data race, все остальные — UB
На мой взгляд, data race — это само по себе и есть соглашение. Соглашение о том, какие конкурирующие инструкции работы с памятью мы считаем легальными, а какие ведут к потенциально нехорошему поведению. Т.е. data race — это и есть название для тех паттернов конкурирующего доступа к памяти, которые порождают что-то нехорошее. А обычное определение «запись и чтение/запись из разных потоков, не упорядоченное SA» — просто показывает, какие конфликты можно разрулить на уровне процессора/контролера памяти/компилятора, а какие конфликты требуют участия программиста, потому что эффективно их разрулить автоматически пока невозможно.
>Барьер я могу пощупать, он материален, он воплощается в инструкции процессора. Об отношениях пусть говорят люди более сведущие, например, А.Вильямс.
Я думаю, это просто С-шный бэкграунд сказывается. В яве к happens-before уже привыкли. И это большой вопрос, на самом деле, что первично — нотация happens-before восходит еще к статье Лампорта из 70-х, когда еще писали в терминах явных сообщений между узлами, а не в терминах shared memory.
Если честно, мне как раз не очень понятно, как вы целостно рассуждаете о корректности алгоритма в терминах барьеров? Да еще и кроссплатформенно — т.е. когда вы не можете явно описать, как именно реализован этот барьер на этой архитектуре, что за конкретные действия за ним стоят. На мой взгляд, нотация относительного порядка (aka happens-before) единственный достаточно универсальный способ рассуждать о взаимодействии потоков, это как раз семантика барьеров должна описываться в терминах happens-before. Правда, я не вдавался особо в глубины C++ MM, но я помню дискуссии в concurrency-interest, где Ханс Боэм писал, что явные барьеры в C-MM оставлены в основном для обратной совместимости, чтобы не нужно было переписывать уже существующие алгоритмы с 0. Но вообще, как я понял, он считает их рудиментом, и довольно опасным рудиментом — с той точки зрения, что с ними сложнее писать корректный кроссплатформенный код.
На мой взгляд, data race — это само по себе и есть соглашение. Соглашение о том, какие конкурирующие инструкции работы с памятью мы считаем легальными, а какие ведут к потенциально нехорошему поведению. Т.е. data race — это и есть название для тех паттернов конкурирующего доступа к памяти, которые порождают что-то нехорошее. А обычное определение «запись и чтение/запись из разных потоков, не упорядоченное SA» — просто показывает, какие конфликты можно разрулить на уровне процессора/контролера памяти/компилятора, а какие конфликты требуют участия программиста, потому что эффективно их разрулить автоматически пока невозможно.
>Барьер я могу пощупать, он материален, он воплощается в инструкции процессора. Об отношениях пусть говорят люди более сведущие, например, А.Вильямс.
Я думаю, это просто С-шный бэкграунд сказывается. В яве к happens-before уже привыкли. И это большой вопрос, на самом деле, что первично — нотация happens-before восходит еще к статье Лампорта из 70-х, когда еще писали в терминах явных сообщений между узлами, а не в терминах shared memory.
Если честно, мне как раз не очень понятно, как вы целостно рассуждаете о корректности алгоритма в терминах барьеров? Да еще и кроссплатформенно — т.е. когда вы не можете явно описать, как именно реализован этот барьер на этой архитектуре, что за конкретные действия за ним стоят. На мой взгляд, нотация относительного порядка (aka happens-before) единственный достаточно универсальный способ рассуждать о взаимодействии потоков, это как раз семантика барьеров должна описываться в терминах happens-before. Правда, я не вдавался особо в глубины C++ MM, но я помню дискуссии в concurrency-interest, где Ханс Боэм писал, что явные барьеры в C-MM оставлены в основном для обратной совместимости, чтобы не нужно было переписывать уже существующие алгоритмы с 0. Но вообще, как я понял, он считает их рудиментом, и довольно опасным рудиментом — с той точки зрения, что с ними сложнее писать корректный кроссплатформенный код.
Да, вы правы, наверное, сказывается C-шный подход. Я не знаток модели памяти явы, слышал только, что в ней применяется модель sequential consistency, и существует довольно обширное её описание. Собственно, при проектировании модели памяти C++ решали две задачи: добиться более компактного описания (за это ратовал, вроде бы, тот же H.Boehm) + большей свободы выбора (= большей эффективности кода, где это можно).
Как я рассуждаю в терминах барьеров — хороший вопрос. На самом деле, все довольно просто: я рассуждаю в терминах абстрактных memory ordering, заданных стандартом, при этом имея в виду, что за ними кроется, — в основном это переупорядочение компилятором (acquire/release-полубарьеры), и только во вторую очередь — процессором. При этом как реализован тот или иной memory ordering на конкретной архитектуре, мне не важно, — я надеюсь на реализацию atomic в STL. К сожалению, мне пришлось спускаться ниже и делать свой atomic-велосипед. Тому было (частично и есть) две причины:
Мыслить в терминах отношений happens-before и пр. у меня как-то не особо получается. Когда вижу чью-либо статью, основанную на отношениях, — кажется, всё понимаю, а вот сам применить на практике — увы… Судя по обилию блогов/заметок о C++11 atomic, такой мозговой клинч наблюдается не только у меня, — многие в разговоре об atomic переходят к рассуждениям о барьерах. Быть может, просто не хватает практики — «об этом надо говорить (и спорить)».
Я согласен, что отношения — более правильный подход. Вот только он слишком абстрактен, приводит к огромным по размеру выкладкам в случае более-менее сложного алгоритма, в котором взаимодействуют более двух atomic, и пока ещё нет инструментов (точнее, только-только появляются первые) по проверке его применения на практике (инструментов верификации).
Проблема чем-то напоминает понятия формальной системы и её интерпретации: можно построить очень интересную формальную теорию, но найти ей интерпретацию, то есть её воплощение в реальном мире, бывает просто невозможно. Путь познания, как правило, другой: от интерпретации (наблюдаемого в жизни) — к формальному описанию. В нашем частном случае формальная модель — это happeds-before, synchronized-with и пр. отношения, а интерпретация — в конечном счете, банальные барьеры.
Вообще, все сказанное мной в статьях и комментариях, — это мое ИМХО, кое в чем я до конца не уверен. Например, в том, правильно ли я проставляю memory ordering в libcds ;-)
Как я рассуждаю в терминах барьеров — хороший вопрос. На самом деле, все довольно просто: я рассуждаю в терминах абстрактных memory ordering, заданных стандартом, при этом имея в виду, что за ними кроется, — в основном это переупорядочение компилятором (acquire/release-полубарьеры), и только во вторую очередь — процессором. При этом как реализован тот или иной memory ordering на конкретной архитектуре, мне не важно, — я надеюсь на реализацию atomic в STL. К сожалению, мне пришлось спускаться ниже и делать свой atomic-велосипед. Тому было (частично и есть) две причины:
- во времена моих первых шагов не было C++11
- разработчики компиляторов до сих пор, похоже, не сошлись во мнении, как должна быть реализована C++11 MM. На это намекает недавно обнаруженный баг в libcds с использованием Clang + libc++ (родная реализация STL для Clang). Опыт учит — ищи ошибку прежде всего у себя, но странное поведение, — крах в однопоточном коде, где всё должно работать и на relaxed atomic, — наводит на мысль, что дело все-таки в компиляторе
Мыслить в терминах отношений happens-before и пр. у меня как-то не особо получается. Когда вижу чью-либо статью, основанную на отношениях, — кажется, всё понимаю, а вот сам применить на практике — увы… Судя по обилию блогов/заметок о C++11 atomic, такой мозговой клинч наблюдается не только у меня, — многие в разговоре об atomic переходят к рассуждениям о барьерах. Быть может, просто не хватает практики — «об этом надо говорить (и спорить)».
Я согласен, что отношения — более правильный подход. Вот только он слишком абстрактен, приводит к огромным по размеру выкладкам в случае более-менее сложного алгоритма, в котором взаимодействуют более двух atomic, и пока ещё нет инструментов (точнее, только-только появляются первые) по проверке его применения на практике (инструментов верификации).
Проблема чем-то напоминает понятия формальной системы и её интерпретации: можно построить очень интересную формальную теорию, но найти ей интерпретацию, то есть её воплощение в реальном мире, бывает просто невозможно. Путь познания, как правило, другой: от интерпретации (наблюдаемого в жизни) — к формальному описанию. В нашем частном случае формальная модель — это happeds-before, synchronized-with и пр. отношения, а интерпретация — в конечном счете, банальные барьеры.
Вообще, все сказанное мной в статьях и комментариях, — это мое ИМХО, кое в чем я до конца не уверен. Например, в том, правильно ли я проставляю memory ordering в libcds ;-)
>Я не знаток модели памяти явы, слышал только, что в ней применяется модель sequential consistency, и существует довольно обширное её описание.
Да, канонически в яве все synchronization actions действительно имеют SC-семантику. Модель сама по себе не такая уж обширная. Обширное описание, скорее, есть у причин почему она такая, какая есть, и как к этому пришли — с этой точки зрения, уверен, описание модели C++ будет только еще более обширным. Но есть такая тонкость, что в яве нет undefined behavior по изначальному дизайну языка. Потому примерно половина объема (и 3/4 сложности) модели памяти в яве это именно попытка задать, пусть очень сложную, но все-таки определенную семантику даже коду с гонками. Попытка эта, в общем-то, провалилась — через пару лет после публикации и реализации в этой части были обнаружены баги, которые не позволяли реализовывать важные оптимизации, поэтому существующие реализации JVM фактически нарушают спецификацию где-то в темных углах кода с data race. Есть несколько предложений, как исправить ошибки, но все они не совместимы с текущей версией JMM, поэтому пока все просто закрывают на это глаза. Как я понимаю, этот фэйл является одной из причин почему сейчас гуру concurrency (Ханс Боэм, Даг Ли, и прочие) в один голос повторяют «data race is evil».
Если не брать эту темную сторону, то оригинальная JMM ни разу не сложнее CMM, даже проще — потому что есть только два варианта memory_ordering: relaxed/SC, причем используемый вариант привязан к типу переменной изначально, а не к конкретной операции доступа: есть volatile переменные, все операции с которыми всегда SC, и есть обычные переменные, которые всегда relaxed. Это, собственно, второй ее недостаток — очевидно, что SC несовместимо со scalability, без введения чего-то типа acquire/release/consume нереально линейно масштабироваться дальше пары десятков процессоров. Фактически же, аналоги acquire/release/consume операций уже некоторое время имеются в яве, но это полулегальные операции, потому что официального апдейта JMM с их формализацией нет и не предвидится.
>Мыслить в терминах отношений happens-before и пр. у меня как-то не особо получается.
Ну, среди явистов тоже очень многие рассуждают в терминах барьеров. Как эвристические рассуждения это неплохо, но суть в том, что если вы попытаетесь сделать рассуждения про барьеры и возможные перестановки более строгим — вы, собственно, и получите happens-before notation. Так что лучше уж, как мне кажется, идти сюда сразу же, как вы поймали общую идею алгоритма, и начинаете думать про реализацию.
> В нашем частном случае формальная модель — это happeds-before, synchronized-with и пр. отношения, а интерпретация — в конечном счете, банальные барьеры.
Я думаю, что здесь вы как раз ошибаетесь. Процессоры не господом богом с неба спущены — они разрабатываются инженерами под нужды разработчиков. Я где-то читал, что при разработке JMM были случаи, когда разработчики Intel подправляли спецификацию своих процессоров по итогам обсуждения — и это вполне логично, ибо кому нужны процессоры с набором команд, с которыми неудобно и ненадежно программировать? Судьба пресловутой Alpha очень наглядна в этом смысле. Разумеется, это двусторонний диалог, но это именно диалог — в отличие от законов природы, с которыми особо-то не подискутируешь.
Например, абсолютное большинство современных general purposes процессоров создает иллюзию SC в однопоточном случае — хотя реально они все суперскалярные и используют внеочередное исполнение команд — то есть поддержание иллюзии SC-исполнения на самом деле стоит немалого гемороя их инженерам. Зачем они идут на этот геморой? — Потому что у процессора с менее тривиальной моделью исполнения будут большие проблемы с продажами. Наглядный пример того, как именно процессоры делаются под концепцию, а не наоборот.
… Вообще, у меня есть мнение, что дело здесь не в сложности именно HB, а в том, что программисты сейчас вообще отвыкли серьезно относиться к надежности своего кода. К тому, что корректность алгоритма нужно доказывать, а не «жопой чуять». Если вы когда-нибудь пробовали доказывать корректность однопоточных алгоритмов, вы должны бы заметить, что разница в сложности не такая уж большая. Но для однопоточного кода отладка и тестирование довольно дешевы, дешевле, чем формальное доказательство — уже целое поколение (я в их числе) выросло на идеологии «достаточное количество юнит-тестов является доказательством корректности программы». И когда оказывается, что для многопоточного случая все это на порядки менее эффективно, и мы снова сталкиваемся с необходимостью формального доказательства — вот тут-то и возникает ощущение огромной сложности.
В частности, лично мне кажется, что основной фокус при создании конкурентных алгоритмов должен быть не на том, как избежать возни с формальным доказательством, а на том, как а) избежать многопоточности вообще б) если уж удалось — сделать алгоритм настолько простым, чтобы ошибиться было просто негде. Потому что сколько либо сложный конкурентный алгоритм требует столько внимательности, проверок и перепроверок для своего написания, что это определенно не работа для одного человека. Тут нужно несколько очень опытных специалистов для постоянного ревью, и месяцы тестирования. Это слишком дорого для личных целей, это оправдано либо в качестве обучения, либо в составе очень популярных фреймворков, вокруг которых сильное коммьюнити.
Да, канонически в яве все synchronization actions действительно имеют SC-семантику. Модель сама по себе не такая уж обширная. Обширное описание, скорее, есть у причин почему она такая, какая есть, и как к этому пришли — с этой точки зрения, уверен, описание модели C++ будет только еще более обширным. Но есть такая тонкость, что в яве нет undefined behavior по изначальному дизайну языка. Потому примерно половина объема (и 3/4 сложности) модели памяти в яве это именно попытка задать, пусть очень сложную, но все-таки определенную семантику даже коду с гонками. Попытка эта, в общем-то, провалилась — через пару лет после публикации и реализации в этой части были обнаружены баги, которые не позволяли реализовывать важные оптимизации, поэтому существующие реализации JVM фактически нарушают спецификацию где-то в темных углах кода с data race. Есть несколько предложений, как исправить ошибки, но все они не совместимы с текущей версией JMM, поэтому пока все просто закрывают на это глаза. Как я понимаю, этот фэйл является одной из причин почему сейчас гуру concurrency (Ханс Боэм, Даг Ли, и прочие) в один голос повторяют «data race is evil».
Если не брать эту темную сторону, то оригинальная JMM ни разу не сложнее CMM, даже проще — потому что есть только два варианта memory_ordering: relaxed/SC, причем используемый вариант привязан к типу переменной изначально, а не к конкретной операции доступа: есть volatile переменные, все операции с которыми всегда SC, и есть обычные переменные, которые всегда relaxed. Это, собственно, второй ее недостаток — очевидно, что SC несовместимо со scalability, без введения чего-то типа acquire/release/consume нереально линейно масштабироваться дальше пары десятков процессоров. Фактически же, аналоги acquire/release/consume операций уже некоторое время имеются в яве, но это полулегальные операции, потому что официального апдейта JMM с их формализацией нет и не предвидится.
>Мыслить в терминах отношений happens-before и пр. у меня как-то не особо получается.
Ну, среди явистов тоже очень многие рассуждают в терминах барьеров. Как эвристические рассуждения это неплохо, но суть в том, что если вы попытаетесь сделать рассуждения про барьеры и возможные перестановки более строгим — вы, собственно, и получите happens-before notation. Так что лучше уж, как мне кажется, идти сюда сразу же, как вы поймали общую идею алгоритма, и начинаете думать про реализацию.
> В нашем частном случае формальная модель — это happeds-before, synchronized-with и пр. отношения, а интерпретация — в конечном счете, банальные барьеры.
Я думаю, что здесь вы как раз ошибаетесь. Процессоры не господом богом с неба спущены — они разрабатываются инженерами под нужды разработчиков. Я где-то читал, что при разработке JMM были случаи, когда разработчики Intel подправляли спецификацию своих процессоров по итогам обсуждения — и это вполне логично, ибо кому нужны процессоры с набором команд, с которыми неудобно и ненадежно программировать? Судьба пресловутой Alpha очень наглядна в этом смысле. Разумеется, это двусторонний диалог, но это именно диалог — в отличие от законов природы, с которыми особо-то не подискутируешь.
Например, абсолютное большинство современных general purposes процессоров создает иллюзию SC в однопоточном случае — хотя реально они все суперскалярные и используют внеочередное исполнение команд — то есть поддержание иллюзии SC-исполнения на самом деле стоит немалого гемороя их инженерам. Зачем они идут на этот геморой? — Потому что у процессора с менее тривиальной моделью исполнения будут большие проблемы с продажами. Наглядный пример того, как именно процессоры делаются под концепцию, а не наоборот.
… Вообще, у меня есть мнение, что дело здесь не в сложности именно HB, а в том, что программисты сейчас вообще отвыкли серьезно относиться к надежности своего кода. К тому, что корректность алгоритма нужно доказывать, а не «жопой чуять». Если вы когда-нибудь пробовали доказывать корректность однопоточных алгоритмов, вы должны бы заметить, что разница в сложности не такая уж большая. Но для однопоточного кода отладка и тестирование довольно дешевы, дешевле, чем формальное доказательство — уже целое поколение (я в их числе) выросло на идеологии «достаточное количество юнит-тестов является доказательством корректности программы». И когда оказывается, что для многопоточного случая все это на порядки менее эффективно, и мы снова сталкиваемся с необходимостью формального доказательства — вот тут-то и возникает ощущение огромной сложности.
В частности, лично мне кажется, что основной фокус при создании конкурентных алгоритмов должен быть не на том, как избежать возни с формальным доказательством, а на том, как а) избежать многопоточности вообще б) если уж удалось — сделать алгоритм настолько простым, чтобы ошибиться было просто негде. Потому что сколько либо сложный конкурентный алгоритм требует столько внимательности, проверок и перепроверок для своего написания, что это определенно не работа для одного человека. Тут нужно несколько очень опытных специалистов для постоянного ревью, и месяцы тестирования. Это слишком дорого для личных целей, это оправдано либо в качестве обучения, либо в составе очень популярных фреймворков, вокруг которых сильное коммьюнити.
точнее, кэшу, — процессор взаимодействует с внешним миром только через кэш
А как-же _mm_stream_ps и иже с ними :)
Большое спасибо за эту серию постов! Очень мало информации по этой теме на русском языке, тем более с попыткой объяснить на нескольких уровнях абстракций (от нутрей ЦПУ до C++) более-менее доступным языком. Надо отметить, что Ваш цикл не (с)только про lock-free, а, скорее, широко охватывает окружающий эту тему контекст.
В IA-64 это зовётся «bundle».
Ещё одна особенность широкого машинного слова — писать на ассемблере для такой архитектуры не самое благодарное занятие. На эффективность кода рассчитывать не стоит, на его читаемость — тоже.
Как говорится, история в сослагательном наклонении не существует. Кто знает, чем будущее обернётся? Вот, например, российский «Эльбрус» — тоже VLIW.
по “пучкам” VLIW (не помню, как это называется в Итаниуме, но перевод – “пучок” – запомнился)
В IA-64 это зовётся «bundle».
То, что современные процессоры делают сами, — загружают свои исполнительные блоки, переупорядочивая операции, — в Итаниуме было доверено компилятору. Но компиляторы не справились с такой задачей и генерировали (и до сих пор генерируют) не слишком оптимальный код.
Ещё одна особенность широкого машинного слова — писать на ассемблере для такой архитектуры не самое благодарное занятие. На эффективность кода рассчитывать не стоит, на его читаемость — тоже.
Так что Itanium – это наше нереализованное будущее.
Как говорится, история в сослагательном наклонении не существует. Кто знает, чем будущее обернётся? Вот, например, российский «Эльбрус» — тоже VLIW.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Lock-free структуры данных. Основы: Модель памяти