Спасибо за отзыв и за интересную поднятую тему, которая позволит лишний раз копнуть чуть глубже.
Вы абсолютно правы, в большинстве случаев сборщики ничего не удаляют, а только двигают туда-сюда достижимые (они же "выжившие") объекты, поэтому термин "удаление объекта" может выглядеть не самым удачным для описания их работы.
Но в продвинутых GC, как это часто бывает у нас в компьютерах, всё сложннее, чем может показаться с первого взгляда. Давайте отложим самые распространенные сценарии выделения / высвобождения памяти и вспомним, например, про существование SoftReference и WeakReference. В отношении них GC имеет больше свободы и может самостоятельно удалить на них ссылку и перевести из разряда достижимых в мусор. Добавим к этому умение современных GC возвращать память операционной системе после уплотнения объектов. В итоге получим, что в некоторых случаях GC может реально удалить даже достижимый объект (вернуть размещающую его страницу памяти операционке), не то что мусор.
Если же говорить не про технические детали и не пытаться всё формализовать, то можно заметить, что термин "удаление объектов" просто давно уже прижился в описании сборщиков (документация Oracle, RedHat, IBM и практически любая другая). Как, например, "удаление файла" на диске или "удаление записи" в БД, которые на деле практически никогда не приводят к реальному удалению соответствующих данных.
Хотя, повторюсь, ваше замечание в целом верное. Может я даже подправлю текст в некоторых местах при очередной ревизии.
Так как в CMS существуют очистки только старшего поколения (без очистки младшего), могут возникать такие ситуации:
У вас существует уже давно перенесенный в старшее поколение объект (назовем его O), на который существуют ссылки только из других объектов старшего поколения.
Вы создали новый объект (назовем его Y), который был размещен в младшем поколении. При конструировании этого объекта вы передали ему ссылку на O, которую он сохранил в одном из своих полей.
Все остальные ссылки на объект O были "забыты", теперь Y является единственным обладателем ссылки на него.
В этот момент была инициирована сборка старшего поколения.
И вот тут возникает та самая ситуация, о которой идет речь в приведенном абзаце. На объект O нет ссылок из "классических" корней -- ни на стеке, ни из статических полей каких-либо классов ссылок на него не осталось. Но при этом объект O не должен считаться мертвым, ведь на него есть ссылка из размещенного в младшем поколении объекта Y. То есть поле объекта Y, размещенного в младшем поколении, выступает в роли корня.
В обычной полной сборке у вас корнем выступала бы ссылка на стеке напрямую на Y (если бы сборка застала нас в тот момент, когда Y был только создан и у нас была бы локальная переменная со ссылкой на него), или на какой-нибудь другой объект, который бы хранил ссылку на Y и т. п. Цепочка от корня до O была бы длиннее. Но для ее составления требовался бы анализ младшего поколения, который является частью полной сборки.
А так как в CMS в данном случае мы рассматриваем не полную сборку, такой анализ не производится, а просто все объекты в младшем поколении считаются "корнями". Если говорить совсем формально, то корнями являются поля-ссылки таких объектов, а не сами объекты, но сути это не меняет.
Нет, на уровне приложения узнать о работе Pacing'а не получится.
Технически он представляет собой маленькую паузу (по умолчанию не больше 10 мсек), которая вставляется в метод запроса TLAB'а из кучи. Такие паузы то появляются, то исчезают, динамически меняют длительность. О них сборщик никого не уведомляет, только в gclog потом выводит общую статистику об их использовании.
Думаю, реализовывать back pressure лучше опираясь на какие-нибудь другие, более устойчивые к настройкам JVM, сигналы и метрики, не полагаясь на внутреннее устройство сборщика, чтобы ничего не поломалось при переключении на другой сборщик.
Технически, конечно, это будет работать. Но обычно даже когда разрабатывают сервисы, которые могут мириться с периодическими рестартами отдельных подов, не рассчитвают на то, что рестарты будут настолько частыми. Если вы изначально не разрабатываете приложение с таким расчетом, чтобы оно очень мало мусорило (а это очень сложно), то падать по OOM с Epsilon'ом оно будет очень часто.
Либо вам придется выделать ему память с очень большим запасом, что намного дороже, чем подобрать сборщик, разменивающий относительно небольшой перерасход памяти и процессора на эффективную сборку, и жить с ним.
То есть за крайне редкими исключениями, я думаю, описанный вами подход будет заметно более дорогим, чем при использовании другого сборщика.
Оркестратор и JVM управляют памятью на разных уровнях. Оркестратор может выделить контейнеру с Java-процессом нужный объем памяти, но он никак не вмешивается в ее дальнейшее использование, он ничего не знает про Java-объекты, кучу, сборку мусора и т. п., это не его зона ответственности. Это уже задача JVM использовать выделеннную ей память для организации в рамках нее всего перечисленного.
Выбор сборщика в большей степени зависит от специфики самого приложения (от требований к нему и от того, как оно работает с памятью), нежели от того, в какой инфраструктуре вы его запускаете. Нужно только учитывать ограничения на доступные JVM ресурсы, которые накладывает инфраструктура, а в остальном смотрите на само приложение, однозначного ответа здесь нет.
Нужно только помнить про особенности работы ZGC, который из-за использования цветных указателей (см. предыдущую статью) может репортить трехкратное значение используемой памяти, что может ставить в тупик какие-нибудь системы контейнеризации или системы их мониторинга. Да и просто людей может смущать.
Не очень понял, на основании чего вы сделали такой вывод. Процесс Java использует те ресурсы, которые вы ему выделили. При желании можете ограничивать как считаете нужным.
терабайтные кучи
16 ТБ - это ограничение сверху, а не минимальное требование. Можете спокойно использовать ZGC и с мелкими кучами.
использование процессорного механизма виртуальной памяти
Виртуализацию памяти используют все прикладные процессы, на каком бы языке вы их не написали. Так работают современные компьютеры. Не очень понимаю, в чем у вас тут претензия к Java.
немного неактуально уже во время популярности микросервисов и относительно маленьких быстрозапускаемых контейнеров.
Микросервисы - это про маленькие зоны ответственноси, а не про маленькие объемы оперативной памяти.
Java идет своим особым путем
В данном случае особый путь Java только в том, чтобы предоставлять разработчику на выбор больше вариантов сборщиков, чтобы можно было подобрать подходящий даже в случае достаточно специфических требований. А сервисы с такими требованиями будут всегда, независимо от того, что сегодня популярно в мейнстриме. Другие платформы, действительно, так не делают.
На самом деле, идея ограничивать возможность продвижения таких объектов в старшее поколение не несет практически никаких преимуществ. Редко используемый softly reachable объект может жить в памяти долго только при условии, что у приложения достаточно много памяти, чтобы позволить себе поддерживать его жизнеспособность. И это хорошо, ведь это кэш, объект может ведь и понадобиться рано или поздно. А как только памяти станет не хватать, такие объекты постепенно начнут выдавливаться из памяти в порядке возрастания частоты использования.
Кроме того, оставлять долгоживующие объекты в младшем поколении накладно — их нужно постоянно копировать при очистке, отслеживать ссылки из них. Да и в плане размера поколение ведь не резиновое. Если место в нем занимают такие объекты, это значит, что другие объекты будут заполнять оставшееся место быстрее, сборки будут выполняться чаще, объекты будут переводиться в старшее поколение быстрее. Даже те, которые при иных обстоятельствах этого не заслужили бы. И это, в свою очередь, будет приводить к более частым полным сборкам, чего как раз и хочется избежать.
Нет, не отличается. Вы написали, что не можете найти подтверждение тому, что softly reachable объекты переходят в старшее поколение. И в качестве такого подтверждения, помимо указаний на технические детали реализации, я хотел донести мысль, что если бы им было запрещено туда переходить, то их основная цель (создание кэшей, гибко подстраивающихся под имеющиеся объемы памяти) не достигалась бы и они просто дублировали бы поведение weakly reachable объектов.
нигде не могу найти подтверждение этому, только немного здесь
Как я выше написал, четкой спецификации на поведение таких ссылок нет. Разные коллекторы могут обрабатывать их по-разному. Все имеющиеся к ним требования (по сути, всего одно требование) описаны в документации на SoftReference, они же упоминаются в ответе по приведенной вами ссылке.
Но описание опции SoftRefLRUPolicyMSPerMB дает чуть больше информации об обработке таких объектов в HotSpot. В частности, что время жизни softly referenced объектов зависит от частоты их использования и от объема свободной памяти. Но никак не от того, в каком поколении находятся соответствующие объекты. Без возможности перемещения в старшее поколение они бы не отличались от weak reference объектов и кэширование на их основе было бы менее эффективным.
Здесь на всякий случай хотелось бы разобраться с терминологией. Я думаю, вопрос касается не soft/weak references самих по себе, а softly/weakly reachable объектов. При этом важно понимать, что само по себе наличие soft/weak ссылки на объект не делает автоматически этот объект softly/weakly reachable. Таковым его делает только дополнительное отсутствие более сильных ссылок.
И вот к этому моменту, когда более сильных ссылок не осталось и объект стал softly/weakly reachable, он уже может находиться в любом поколении. Так что ответ на второй вопрос формально «нет, они не всегда в молодом поколении». Но если рассматривать случай, когда на объект изначально не существовало никаких ссылок, кроме weak, он не перейдет в более старшее поколение, так как ссылка на него будет обнулена при первой же сборке мусора.
Что касается softly reachable объектов, по ним у GC есть только одно формальное требование — обнулить их перед выбрасыванием OOM в рамках последней попытки освободить память. Но при этом нет никакого запрета на то, чтобы они вели себя полностью аналогично weak reachable. На практике, конечно, GC старается найти золотую середину, не выбрасывая их сразу при обнаружении, но и не оттягивая очистку до последнего. Поэтому такие объекты спокойно переходят в старшее поколение если недостатка в памяти нет. Посмотрите описание опции SoftRefLRUPolicyMSPerMB, она регулирует поведение GC в части определения, когда уже можно удалять softly reachable объекты.
С системами управления версиями сами по себе TLA+ спецификации вполне уживаются, ведь вы просто редактируете текстовый файл. Да, часть этого файла за вас редактирует IDE при трансляции алгоритма (но только если вы используете PlusCal), но для системы контроля версий ведь не важно, кто его отредактировал.
Есть только два нюанса, связанные с тем, что а) Toolbox хранит некоторые настройки в файле *.launch, который сам создает в отдельной поддиректории {имя спека}.toolbox, б) в этой же поддиректории TLC формирует дополнительные файлы во время проверки. Но с этой структурой нужно один раз разобраться и корректно настроить .gitignore, а также флажки для отключения этих файлов. После этого можно работать.
Компиляции как таковой не происходит, это не язык программирования. Здесь просто происходит трансляция алгоритма на PlusCal в спецификацию TLA+ и производится проверка (обычная синтаксическая) этой спецификации.
Частью тулбокса является библиотека tla2tools.jar, в которой как раз и содержатся инструменты, с помощью которых можно производить трансляцию, проверку и запуск TLC.
Соответственно, можно запускать это все из командной строки. Есть готовые скрипты, в которые удобно завернуты основные вызовы: tla-bin.
На скриншоте приведен свернутый Error-Trace, в котором видна только последовательность шагов, которые приводят к проблеме. На самом деле каждый шаг можно развернуть и посмотреть значения всех переменных на этом шаге.
То есть вы подали TLC на вход алгоритм и описание свойств, которым вы бы хотели, чтобы он удовлетворял. А TLC проверил алгоритм и сказал вам, действительно ли он им удовлетворяет. И если не удовлетворяет, то отображает конкретный пример, который нарушает как минимум одно из ожидаемых свойств.
После этого вы уже анализируете этот конкретный проблемный пример и (в идеале) понимаете, что вы не учли в алгоритме. Правите алгоритм и повторяете проверку.
Команда File -> Translate PlusCal Algorithm. Горячие клавиши по умолчанию Ctrl + T (Cmd + T на маке). Можно настроить автоматическую трансляцию при сохранении файла.
Раз уж статья про российский рынок ценных бумаг, стоит упомянуть и Санкт-Петербургскую фондовую биржу, на которой торгуются в том числе акции крупных иностранных компаний.
Это Ньелю, работодатель Ле Страдика, может подать такой иск. А перед Залуски у Ле Страдика нет никаких обязательств и он никаких прав Залуски не нарушал и никакого ущерба ему не причинял. Даже если бы он явно рассказал Залуски всю эту информацию, он бы провинился перед компанией Iliad и перед регулятором за разглашение, но не перед Залуски.
Залуски по факту получения этой информации тоже ничего не нарушил (если только не будет доказано, что он специально шпионил). Он мог бы спокойно жить дальше с этим знанием, дожидаясь официального раскрытия этой информации и будучи добропорядочным гражданином. Но он решил поделиться информацией со своим коллегой (справедливо полагая, что это могут быть очень важные и пока никому не известные сведения), нарушив правила регуляции и положив начало дальнейшей цепочке неправомерного распространения этой информации. Но это тоже могло бы сойти ему с рук, если бы Лезье, уже будучи специалистом в этой сфере и точно понимая, что это инсайд, не начал бы распространять эту информацию и дальше, а просто посоветовал бы Залуски больше об этом ни с кем не говорить. Поэтому штраф Залуски заметно меньше, чем Лезье.
В разных ветках обсуждается примерно одно и то же и проводятся, как мне кажется, не совсем верные аналогии. Вынесу в отдельную ветку свои рассуждения.
TLDR
Информация, полученная Залуски, является инсайдерской.
При этом никакой инсайдерской сделки в данном эпизоде не было и обвинений в этом нет.
Суть претензий регулятора к Залуски, его коллеге Лезье и USB сводится к неправомерному распространению упомянутой инсайдерской информации.
К Ле Страдику, допустившему утечку информации, конкретно у регулятора претензий нет. Они могут быть у его работодателя.
Детальнее
Расследованием инцидента занимается AMF (французский регулятор финансовых рынков). Это значит, что он может руководствоваться положениями регуляций MAD II (действовавшей на момент описываемых сообытий) и MAR (действующих в настоящее время). Принципиальной разницы в этой части между ними нет.
Согласно этим регуляциям, информация о планируемом крупном предложении покупки T-Mobile компанией Iliad является инсайдерской. Эта информация на тот момент не являлась публичной, она относилась к планам по крупной сделке поглощения, она могла оказать существенное влияние на стоимость ценных бумаг акционерной компании (акции Iliad SA находятся в свободном обращении). Эта информация в том числе была признана инсайдерской в рамках более общего дела об инсайдерской торговле со стороны топ-менеджера самой Iliad.
Согласно этим же регуляциям, к неправомерным действиям с такой информацией относится не только совершение операций на финансовых рынках с бумагами соответствующей компании, но и передача такой информации третьим лицам — MAD II Article 4(2) или MAR Article 10(1).
В данном случае факта инсайдерской торговли (операций на финансовых рынках с ценными бумагами Iliad SA) не было, об этом явно сказано и в самой статье и в переводе. Предложение кредита такой сделкой не является. Не понимаю, почему в комментариях все упорно делают акцент именно на этом предложении от UBS, не обращая внимание на суть обвинений.
А вот распространение инсайдерской информации было, в нем как раз и обвиняют Залуски, который передал ее Лезье. И самому Лезье, который дальше, видимо, пустил ее по UBS. И сам UBS за такое поведение сотрудников тоже хотят оштрафовать.
Ле Страдик, видимо, смог убедить регулятора, что с его стороны утечка информации произошла непреднамеренно, поэтому его регулятор штрафовать не предлагает. С ним, по идее, должен разбираться его работодатель. Может в суд подать за такое небрежное обращение с инсайдом. А может простить, это их дело.
Сама новость недельной давности. Это описываемые события относятся к 2014 году.
MAR, Article 10(1): For the purposes of this Regulation, unlawful disclosure of inside information arises where a person possesses inside information and discloses that information to any other person, except where the disclosure is made in the normal exercise of an employment, a profession or duties.
Спасибо за отзыв и за интересную поднятую тему, которая позволит лишний раз копнуть чуть глубже.
Вы абсолютно правы, в большинстве случаев сборщики ничего не удаляют, а только двигают туда-сюда достижимые (они же "выжившие") объекты, поэтому термин "удаление объекта" может выглядеть не самым удачным для описания их работы.
Но в продвинутых GC, как это часто бывает у нас в компьютерах, всё сложннее, чем может показаться с первого взгляда. Давайте отложим самые распространенные сценарии выделения / высвобождения памяти и вспомним, например, про существование SoftReference и WeakReference. В отношении них GC имеет больше свободы и может самостоятельно удалить на них ссылку и перевести из разряда достижимых в мусор. Добавим к этому умение современных GC возвращать память операционной системе после уплотнения объектов. В итоге получим, что в некоторых случаях GC может реально удалить даже достижимый объект (вернуть размещающую его страницу памяти операционке), не то что мусор.
Если же говорить не про технические детали и не пытаться всё формализовать, то можно заметить, что термин "удаление объектов" просто давно уже прижился в описании сборщиков (документация Oracle, RedHat, IBM и практически любая другая). Как, например, "удаление файла" на диске или "удаление записи" в БД, которые на деле практически никогда не приводят к реальному удалению соответствующих данных.
Хотя, повторюсь, ваше замечание в целом верное. Может я даже подправлю текст в некоторых местах при очередной ревизии.
Так как в CMS существуют очистки только старшего поколения (без очистки младшего), могут возникать такие ситуации:
У вас существует уже давно перенесенный в старшее поколение объект (назовем его
O), на который существуют ссылки только из других объектов старшего поколения.Вы создали новый объект (назовем его
Y), который был размещен в младшем поколении. При конструировании этого объекта вы передали ему ссылку наO, которую он сохранил в одном из своих полей.Все остальные ссылки на объект
Oбыли "забыты", теперьYявляется единственным обладателем ссылки на него.В этот момент была инициирована сборка старшего поколения.
И вот тут возникает та самая ситуация, о которой идет речь в приведенном абзаце. На объект
Oнет ссылок из "классических" корней -- ни на стеке, ни из статических полей каких-либо классов ссылок на него не осталось. Но при этом объектOне должен считаться мертвым, ведь на него есть ссылка из размещенного в младшем поколении объектаY. То есть поле объектаY, размещенного в младшем поколении, выступает в роли корня.В обычной полной сборке у вас корнем выступала бы ссылка на стеке напрямую на
Y(если бы сборка застала нас в тот момент, когдаYбыл только создан и у нас была бы локальная переменная со ссылкой на него), или на какой-нибудь другой объект, который бы хранил ссылку наYи т. п. Цепочка от корня доOбыла бы длиннее. Но для ее составления требовался бы анализ младшего поколения, который является частью полной сборки.А так как в CMS в данном случае мы рассматриваем не полную сборку, такой анализ не производится, а просто все объекты в младшем поколении считаются "корнями". Если говорить совсем формально, то корнями являются поля-ссылки таких объектов, а не сами объекты, но сути это не меняет.
Нет, на уровне приложения узнать о работе Pacing'а не получится.
Технически он представляет собой маленькую паузу (по умолчанию не больше 10 мсек), которая вставляется в метод запроса TLAB'а из кучи. Такие паузы то появляются, то исчезают, динамически меняют длительность. О них сборщик никого не уведомляет, только в gclog потом выводит общую статистику об их использовании.
Думаю, реализовывать back pressure лучше опираясь на какие-нибудь другие, более устойчивые к настройкам JVM, сигналы и метрики, не полагаясь на внутреннее устройство сборщика, чтобы ничего не поломалось при переключении на другой сборщик.
Технически, конечно, это будет работать. Но обычно даже когда разрабатывают сервисы, которые могут мириться с периодическими рестартами отдельных подов, не рассчитвают на то, что рестарты будут настолько частыми. Если вы изначально не разрабатываете приложение с таким расчетом, чтобы оно очень мало мусорило (а это очень сложно), то падать по OOM с Epsilon'ом оно будет очень часто.
Либо вам придется выделать ему память с очень большим запасом, что намного дороже, чем подобрать сборщик, разменивающий относительно небольшой перерасход памяти и процессора на эффективную сборку, и жить с ним.
То есть за крайне редкими исключениями, я думаю, описанный вами подход будет заметно более дорогим, чем при использовании другого сборщика.
Оркестратор и JVM управляют памятью на разных уровнях. Оркестратор может выделить контейнеру с Java-процессом нужный объем памяти, но он никак не вмешивается в ее дальнейшее использование, он ничего не знает про Java-объекты, кучу, сборку мусора и т. п., это не его зона ответственности. Это уже задача JVM использовать выделеннную ей память для организации в рамках нее всего перечисленного.
Выбор сборщика в большей степени зависит от специфики самого приложения (от требований к нему и от того, как оно работает с памятью), нежели от того, в какой инфраструктуре вы его запускаете. Нужно только учитывать ограничения на доступные JVM ресурсы, которые накладывает инфраструктура, а в остальном смотрите на само приложение, однозначного ответа здесь нет.
Нужно только помнить про особенности работы ZGC, который из-за использования цветных указателей (см. предыдущую статью) может репортить трехкратное значение используемой памяти, что может ставить в тупик какие-нибудь системы контейнеризации или системы их мониторинга. Да и просто людей может смущать.
Не очень понял, на основании чего вы сделали такой вывод. Процесс Java использует те ресурсы, которые вы ему выделили. При желании можете ограничивать как считаете нужным.
16 ТБ - это ограничение сверху, а не минимальное требование. Можете спокойно использовать ZGC и с мелкими кучами.
Виртуализацию памяти используют все прикладные процессы, на каком бы языке вы их не написали. Так работают современные компьютеры. Не очень понимаю, в чем у вас тут претензия к Java.
Микросервисы - это про маленькие зоны ответственноси, а не про маленькие объемы оперативной памяти.
В данном случае особый путь Java только в том, чтобы предоставлять разработчику на выбор больше вариантов сборщиков, чтобы можно было подобрать подходящий даже в случае достаточно специфических требований. А сервисы с такими требованиями будут всегда, независимо от того, что сегодня популярно в мейнстриме. Другие платформы, действительно, так не делают.
На самом деле, идея ограничивать возможность продвижения таких объектов в старшее поколение не несет практически никаких преимуществ. Редко используемый softly reachable объект может жить в памяти долго только при условии, что у приложения достаточно много памяти, чтобы позволить себе поддерживать его жизнеспособность. И это хорошо, ведь это кэш, объект может ведь и понадобиться рано или поздно. А как только памяти станет не хватать, такие объекты постепенно начнут выдавливаться из памяти в порядке возрастания частоты использования.
Кроме того, оставлять долгоживующие объекты в младшем поколении накладно — их нужно постоянно копировать при очистке, отслеживать ссылки из них. Да и в плане размера поколение ведь не резиновое. Если место в нем занимают такие объекты, это значит, что другие объекты будут заполнять оставшееся место быстрее, сборки будут выполняться чаще, объекты будут переводиться в старшее поколение быстрее. Даже те, которые при иных обстоятельствах этого не заслужили бы. И это, в свою очередь, будет приводить к более частым полным сборкам, чего как раз и хочется избежать.
Как я выше написал, четкой спецификации на поведение таких ссылок нет. Разные коллекторы могут обрабатывать их по-разному. Все имеющиеся к ним требования (по сути, всего одно требование) описаны в документации на SoftReference, они же упоминаются в ответе по приведенной вами ссылке.
Но описание опции SoftRefLRUPolicyMSPerMB дает чуть больше информации об обработке таких объектов в HotSpot. В частности, что время жизни softly referenced объектов зависит от частоты их использования и от объема свободной памяти. Но никак не от того, в каком поколении находятся соответствующие объекты. Без возможности перемещения в старшее поколение они бы не отличались от weak reference объектов и кэширование на их основе было бы менее эффективным.
И вот к этому моменту, когда более сильных ссылок не осталось и объект стал softly/weakly reachable, он уже может находиться в любом поколении. Так что ответ на второй вопрос формально «нет, они не всегда в молодом поколении». Но если рассматривать случай, когда на объект изначально не существовало никаких ссылок, кроме weak, он не перейдет в более старшее поколение, так как ссылка на него будет обнулена при первой же сборке мусора.
Что касается softly reachable объектов, по ним у GC есть только одно формальное требование — обнулить их перед выбрасыванием OOM в рамках последней попытки освободить память. Но при этом нет никакого запрета на то, чтобы они вели себя полностью аналогично weak reachable. На практике, конечно, GC старается найти золотую середину, не выбрасывая их сразу при обнаружении, но и не оттягивая очистку до последнего. Поэтому такие объекты спокойно переходят в старшее поколение если недостатка в памяти нет. Посмотрите описание опции SoftRefLRUPolicyMSPerMB, она регулирует поведение GC в части определения, когда уже можно удалять softly reachable объекты.
Есть только два нюанса, связанные с тем, что а) Toolbox хранит некоторые настройки в файле *.launch, который сам создает в отдельной поддиректории {имя спека}.toolbox, б) в этой же поддиректории TLC формирует дополнительные файлы во время проверки. Но с этой структурой нужно один раз разобраться и корректно настроить .gitignore, а также флажки для отключения этих файлов. После этого можно работать.
Частью тулбокса является библиотека tla2tools.jar, в которой как раз и содержатся инструменты, с помощью которых можно производить трансляцию, проверку и запуск TLC.
Соответственно, можно запускать это все из командной строки. Есть готовые скрипты, в которые удобно завернуты основные вызовы: tla-bin.
Есть плагин для VS Code, который использует такие же вызовы: TLA+ for Visual Studio Code.
То есть вы подали TLC на вход алгоритм и описание свойств, которым вы бы хотели, чтобы он удовлетворял. А TLC проверил алгоритм и сказал вам, действительно ли он им удовлетворяет. И если не удовлетворяет, то отображает конкретный пример, который нарушает как минимум одно из ожидаемых свойств.
После этого вы уже анализируете этот конкретный проблемный пример и (в идеале) понимаете, что вы не учли в алгоритме. Правите алгоритм и повторяете проверку.
Залуски по факту получения этой информации тоже ничего не нарушил (если только не будет доказано, что он специально шпионил). Он мог бы спокойно жить дальше с этим знанием, дожидаясь официального раскрытия этой информации и будучи добропорядочным гражданином. Но он решил поделиться информацией со своим коллегой (справедливо полагая, что это могут быть очень важные и пока никому не известные сведения), нарушив правила регуляции и положив начало дальнейшей цепочке неправомерного распространения этой информации. Но это тоже могло бы сойти ему с рук, если бы Лезье, уже будучи специалистом в этой сфере и точно понимая, что это инсайд, не начал бы распространять эту информацию и дальше, а просто посоветовал бы Залуски больше об этом ни с кем не говорить. Поэтому штраф Залуски заметно меньше, чем Лезье.
В разных ветках обсуждается примерно одно и то же и проводятся, как мне кажется, не совсем верные аналогии. Вынесу в отдельную ветку свои рассуждения.
TLDR
Детальнее
Расследованием инцидента занимается AMF (французский регулятор финансовых рынков). Это значит, что он может руководствоваться положениями регуляций MAD II (действовавшей на момент описываемых сообытий) и MAR (действующих в настоящее время). Принципиальной разницы в этой части между ними нет.
Согласно этим регуляциям, информация о планируемом крупном предложении покупки T-Mobile компанией Iliad является инсайдерской. Эта информация на тот момент не являлась публичной, она относилась к планам по крупной сделке поглощения, она могла оказать существенное влияние на стоимость ценных бумаг акционерной компании (акции Iliad SA находятся в свободном обращении). Эта информация в том числе была признана инсайдерской в рамках более общего дела об инсайдерской торговле со стороны топ-менеджера самой Iliad.
Согласно этим же регуляциям, к неправомерным действиям с такой информацией относится не только совершение операций на финансовых рынках с бумагами соответствующей компании, но и передача такой информации третьим лицам — MAD II Article 4(2) или MAR Article 10(1).
В данном случае факта инсайдерской торговли (операций на финансовых рынках с ценными бумагами Iliad SA) не было, об этом явно сказано и в самой статье и в переводе. Предложение кредита такой сделкой не является. Не понимаю, почему в комментариях все упорно делают акцент именно на этом предложении от UBS, не обращая внимание на суть обвинений.
А вот распространение инсайдерской информации было, в нем как раз и обвиняют Залуски, который передал ее Лезье. И самому Лезье, который дальше, видимо, пустил ее по UBS. И сам UBS за такое поведение сотрудников тоже хотят оштрафовать.
Ле Страдик, видимо, смог убедить регулятора, что с его стороны утечка информации произошла непреднамеренно, поэтому его регулятор штрафовать не предлагает. С ним, по идее, должен разбираться его работодатель. Может в суд подать за такое небрежное обращение с инсайдом. А может простить, это их дело.
MAR, Article 10(1): For the purposes of this Regulation, unlawful disclosure of inside information arises where a person possesses inside information and discloses that information to any other person, except where the disclosure is made in the normal exercise of an employment, a profession or duties.