Привет, Хабр. Вашему вниманию предлагается сокращённый перевод эпичного поста под авторством Энди Уорфилда, вице-президента и заслуженного инженера в компании Amazon, занятого разработкой S3. Пост основан на его пленарном выступлении с конференции USENIX FAST ‘23 и затрагивает три различных аспекта, касающихся выстраивания и эксплуатации такого огромного хранилища данных как S3. Если пост окажется интересным - рассмотрим вариант перевести и вторую часть.

17 лет назад, в далёком-далёком университетском кампусе…

История системы S3 начинается 14 марта 2006, а значит, в этом году ей исполняется 17 лет. У меня в голове не укладывается, что для тех программистов, которые сегодня начинают карьеру, S3 (Simple Storage Service = "простой сервис хранения данных") – это просто хранилище данных, существующее в Интернете с тех самых пор, как они познакомились с компьютером. Семнадцать лет назад я ещё только дописывал диссертацию на соискание степени PhD в Кембриджском университете. Трудился в лаборатории, где разрабатывали Xen – опенсорсный гипервизор. Нашлось несколько компаний и в числе их Amazon, которые выстроили на основе Xen первые публичные облака. Наша исследовательская группа из Кембриджа переключилась с академической разработки Xen на развитие собственного стартапа XenSource. Предполагалось, что мы не станем строить на основе Xen очередное публичное облако, а монетизируем технологию, станем продавать её как софт для предприятий. Вы можете отметить, что где-то мы упустили нас шанс. XenSource рос и, в конце концов, его приобрела Citrix. Я же за это время подробно изучил, как развивать команды и растить бизнес (а также договариваться о коммерческом лизинге, ремонтировать отопление, вентиляцию и вытяжку в серверной и пр). В аспирантуре такому не учат.

Но в тот период я был убеждён, что моя цель в жизни – стать университетским профессором. Я пробовал устроиться на нескольких кафедрах и так оказался в Университете Британской Колумбии (UBC) – что оказалось весьма удобно, так как у моей жены уже была работа в Ванкувере, и сам город нам нравится. Я очутился на посту преподавателя и по глупости раздул мою лабораторию до целых 18 студентов, чего ни в коем, слышите, ни в коем случае не рекомендую никому, кто начинает карьеру в качестве ассистент-профессора. Мне льстило возглавлять такую большую лабораторию, в которой полно замечательных людей. Но как же это оказалось изнурительно, курировать такое множество аспирантов одновременно. Уверен, что справлялся с этим из рук вон плохо. Несмотря на это, наша исследовательская лаборатория была потрясающим сообществом коллег, создававших такие вещи, которыми я горжусь по сей день. Мы написали кучу всевозможных (по-настоящему интересных) статей по безопасности, хранению данных, виртуализации и работе с сетями.  

Чуть больше двух лет я успел проработать профессором в Университете Британской Колумбии – и мы с несколькими студентами решили открыть ещё один стартап. Это была компания Coho Data, в которой мы делали ставку на две технологии, которые тогда ещё только зарождались: твердотельные диски NVMe и программируемые Ethernet-коммутаторы. Мы стремились создать высокопроизводительное хранилище данных, рассчитанное на горизонтальное масштабирование. Далее мы дорастили коллектив Coho примерно до 150 человек и открыли офисы в четырёх странах. Опять же, это была возможность изучить многие вещи, например: какова должна быть прочность перекрытий на втором этаже, если там стоят серверы, как устроены аналитические потоки в хедж-фондах Уолл-Стрита. Обе эти темы никак не были связаны с моим преподавательским и исследовательским образованием в области информатики. Опыт работы в Coho получился чудесным и многому меня научил, но, в конце концов, компания не смогла встать на ноги, и нам пришлось её свернуть.

Так мне и довелось вернуться в мой практически опустевший университетский кабинет. Я осознал, что выпустился мой последний аспирант, а сам я не был уверен, что у меня хватит сил вновь выстраивать исследовательскую лабораторию с нуля. Кроме того, меня тянуло попробовать силы на такой профессорской кафедре, где я мог бы преподавать науку об облачных вычислениях. Поэтому решил, что для начала стоит на собственном опыте изучить, как именно они устроены.

Я расспросил об этом некоторых облачных провайдеров. Особенно интересные беседы получились у нас с ребятами из Amazon, и я решил отправиться в эту компанию. Здесь я до сих пор и работаю. Живу в Ванкувере, а моя инженерная специализация требует иметь дело со всем спектром продуктов Amazon для хранения данных. Таким образом, огромную часть рабочего время я провожу, имея дело с S3.

Как устроено хранилище S3

Только придя в Amazon в 2017 году, я позаботился о том, чтобы свой первый рабочий день провести в паре с Сетом Марклом. Сет – один из первопроходцев S3. Он пригласил меня в небольшой кабинет с маркерной доской, а затем в течение шести часов объяснял мне, как работает S3.

Это было изумительно. Мы делали зарисовки, я сыпал вопросами, но ни одним из них не смог озадачить Сета. Он отвечал исчерпывающе, но лучше и не придумаешь. Даже тогда система S3 уже была очень велика, но в самых общих чертах – которые мы рисовали маркерами на доске – она не слишком отличается от большинства прочих систем хранения данных, с которыми вам доводилось иметь дело.

S3 – это сервис для хранения данных в виде объектов, снабжённый HTTP REST API. Здесь есть парк машин клиентской части с REST API, сервис пространства имён, парк хранения данных, представляющий собой уйму жёстких дисков, а также отдельный парк машин, занятых выполнением фоновых операций. В контексте большого предприятия эти фоновые задачи могут называться «сервисы по работе с данными» - таковы, например, репликация данных и многоуровневое их распределение. Что в данном случае интересно: если взглянуть на максимально высокоуровневую схему S3, отражающую, как именно спроектировано хранилище — окажется, что схема воспроизводит корпоративную организацию AWS. Иногда о таком подходе говорят в пренебрежительном ключе, но в данном случае аналогия просто захватывающая. У каждого из этих разнообразных компонентов есть своё место в организации S3. У каждой задачи есть руководитель, а работает над ней несколько команд. Если же перейти на следующий уровень детализации в этой схеме и попытаться раскрыть одну из рамок и содержащиеся в ней компоненты, то обнаружим, что рамка организована по принципу матрёшки: в ней есть вложенные компоненты, к которым приставлены собственные команды, собственные парки машин, и работают они во многом как независимые компании.

Сегодня S3 слагается из сотен микросервисов, которые структурированы именно таким образом. Межкомандные взаимодействия буквально являются контрактами на уровне API. Как и в случае с любым кодом, который приходится писать, иногда можно неверно реализовать модульность, и такие межкомандные взаимодействия получатся несколько неэффективными и угловатыми. Придётся немало поработать, чтобы привести их в порядок, но это неотъемлемая часть разработки ПО, присущая, как оказывается, и сплачиванию команд разработчиков.

Две вещи, которые быстро подмечаешь

До Amazon я имел дело с исследовательским ПО, широко применяемым свободным ПО, а также над ПО для больших предприятий и ещё занимался разработкой устройств; всё это использовалось в продакшене, порой в реально больших компаниях. Но в общем и целом этот софт был продуктом, который мы проектировали, собирали, тестировали и сдавали. Мы этот софт упаковывали и доставляли. Разумеется, мы могли передать вопрос наверх, приходилось обращаться в поддержку, а также мы исправляли баги, выкатывали патчи и обновления, но, в конечном счёте, мы производили софт. Причастность к глобальному сервису хранения данных – это работа совершенно иного порядка. В сущности, S3 – это живой дышащий организм. Каждая его клетка, от разработчиков, пишущих код (далее поступающий на жёсткие диски на самом дне софтверного стека) до монтёров, устанавливающих новые серверные стойки в наших ЦОДах и далее до пользователей, тонко настраивающих приложения ради повышения производительности – все они образуют единую, постоянно развивающуюся систему. Клиенты S3 не покупают софт, они покупают услугу и рассчитывают, что работа с сервисом пойдёт непрерывно, а также просто замечательно.

Первым делом я заметил, что мне придётся поменять, а в сущности – расширить – всё моё понимание софтверных систем и того, каковы они в динамике. Это означает не просто расширить представления о разработке ПО, чтобы научиться учитывать все те сотни микросервисов, из которых состоит S3. Нет, нужно помнить и обо всех людях, участвующих в проектировании, создании, развёртывании и эксплуатации всего этого кода. Всё это одно целое, которое не осмыслить просто как софт. Это софт, хард и люди, а ещё эта система растёт и постоянно развивается.

Второе наблюдение опишу так: несмотря на то, что та схема на маркерной доске лишь широкими мазками представляла организацию и её софт, она могла дать полностью превратное впечатление, поскольку совершенно не отражает всего масштаба этой системы. В каждой из рамок заключена отдельная совокупность горизонтально масштабируемых программных сервисов, которые сами зачастую также складываются из более мелких сервисов. Мне в буквальном смысле потребовались годы, чтобы усвоить истинный масштаб той системы, с которой я работаю, и даже сегодня я порой удивляюсь, какие следствия проистекают из такого масштаба.

S3 в числах (на момент публикации оригинала этого поста).

Технический масштаб: параметры и физика хранения данных

Вероятно, вас не удивляет моё замечание, что S3 — по-настоящему большая система, и что в ней используется МНОГО жёстких дисков. Миллионы. Поэтому, говоря о S3, нелишне будет подробнее обсудить сами жёсткие диски. Жёсткие диски – удивительные устройства и в каком-то отношении всегда были удивительны.

Первый жёсткий диск сконструировал Яков Рабинов (Джейкоб Рэбиноу), работавший в исследовательской организации, из которой впоследствии вырос американский Национальный Институт Стандартов И Технологий (NIST). Рабинов был экспертом по физике магнитов и машиностроению, и ему было поручено сконструировать магнитное хранилище данных на плоских носителях, устроенных подобно книжным страницам. Он решил, что такая идея слишком сложна и неэффективна, поэтому позаимствовал идею вращающейся пластинки с проигрывателя. Так он собрал массив вращающихся магнитных дисков, которые могли считываться всего одной головкой. Чтобы такая система заработала, он вырезал из каждого блина сектор, напоминающий кусочек пиццы, чтобы через этот зазор считывающая головка могла добираться до нужной пластинки. Рабинов

описал этот процесс как «чтение книги, не открывая её». Первый общедоступный жёсткий диск появился в продаже 7 лет спустя, в 1956 году, когда компания IBM задействовала хранилище на 350 дисков в конструкции своей компьютерной системы 305 RAMAC. Чуть ниже мы поговорим о RAMAC подробнее.

Сегодня, через 67 лет после появления жёстких дисков в продаже, они во множестве используются по всему миру. В глобальном масштабе количество байт, записанных на жёстких дисках, продолжает ежегодно расти, но область применения жёстких дисков явно сокращается. Всё меньше и меньше задач решается с их помощью. Сегодня почти все диски, устанавливаемые на пользовательских устройствах, являются твердотельными, такой же переход наблюдается и на многих предприятиях. Джим Грей прогнозировал такой тренд еще в 2006 году, когда провидчески сказал: «С магнитной лентой покончено, теперь диск – это лента. Флэш-память – это диск. Локальность RAM правит бал». В течение двух последних десятилетий эта цитата часто приводилась в обоснование того, что нужно развивать энергонезависимые хранилища данных, но сделанное здесь наблюдение о дисках не менее интересно.

Жёсткие диски больше не являются основным хранилищем данных, поскольку они большие (речь как о габаритах, так и об объёме в байтах), медленные и относительно легко бьются. Практически в любых прикладных задачах, связанных с хранением данных, флэш-память оказывается лучше. Но жёсткий диск – это абсолютный инженерно-инновационный шедевр, и в своих сильных сторонах HDD просто изумительны. Одна из таких сильных сторон – экономичность, и при проектировании такой крупномасштабной системе как S3 открываются уникальные возможности, позволяющие сгладить некоторые ограничения отдельных жёстких дисков.  

Готовясь к выступлению на конференции FAST, я спросил Тима Рауша, не может ли он мне напомнить старинную метафору, касающуюся жёстких дисков – о самолёте, летящем над лужайкой. Тим готовил PhD-диссертацию в Университете Карнеги-Меллона и был одним из первых, кто исследовал диски, работающие по технологии термомагнитной записи (HAMR). Тим на протяжении большей части карьеры занимался жёсткими дисками вообще и HAMR в частности, и мы согласились друг с другом, что метафора с самолётом отлично иллюстрирует как сложность, так и механическую сложность, заключённую в HDD. Приводя такой пример, мы увеличиваем жёсткий диск до размеров авиалайнера, а далее рассуждаем об относительных размерах остальных его компонентов. Вот версия  этой метафоры от 2023 года.

Представьте себе, что головка жёсткого диска – это Боинг-747, летящий над лугом со скоростью 160 километров в час. Воздушный просвет между брюхом самолёта и кончиками травинок сравним с двумя листами бумаги. Теперь, если уподобить разряды на диске кончикам травинок и измерить их, то ширина дорожки составит 4,6 травинок, а длина разряда равна одной травинке. Самолёт, пролетая над лугом, будет подсчитывать травинки, и при этом будет пропускать травинку только 1 раз на каждые 25 000 кругосветных витков.

Это частотность ошибок, равная 1 к 10¹⁵ запросов. В реальных условиях можно наблюдать, что такая травинка пропускается весьма часто – и этот фактор необходимо учитывать при работе с S3.

Теперь давайте вернёмся к самому первому жёсткому диску, IBM RAMAC 1956 года изготовления. Вот выдержка из спецификации этого изделия:

Теперь давайте для сравнения рассмотрим крупнейший HDD, который можно купить на момент публикации оригинала этого поста. Он называется Western Digital Ultrastar DC HC670, ёмкость – 26 ТБ. Со времён RAMAC ёмкость диска увеличилась в 7,2 миллиона раз, тогда как сам жёсткий диск уменьшился в 5000 раз. С поправкой на инфляцию каждый байт подешевел в 6 миллиардов раз. Но, несмотря на всё это, время подвода головок – период, требуемый для произвольного доступа к конкретному фрагменту информации, записанному на диске – улучшился только в 150 раз. Почему? Потому что это механика. Приходится дожидаться, пока сдвинется рычаг, повернётся блин, а эти механические аспекты улучшались далеко не так быстро, как электроника. Если вы совершаете на диске произвольные операции чтения и записи, и механика организована максимально быстро, то можно ожидать примерно 120 операций в секунду. Именно такое число было актуально и в 2006 году, когда начинается история S3, и за десятилетие до того показатель был почти таким же.

Такое несоответствие между ростом ёмкости HDD при долгом плато по показателю производительности – это фактор, наиболее повлиявший на проектирование S3. Чтобы масштабировать количество хранимых байт, приходится максимально активно переходить к использованию максимально объёмистых жёстких дисков. Ёмкость крупнейших современных жёстких дисков составляет 26 ТБ, а, согласно планам развития отрасли, уже в следующем десятилетии мы должны прийти к дискам ёмкостью по 200 ТБ (вдумайтесь, 200 ТБ!). К этому моменту, если удастся максимально равномерно распределить произвольный доступ по всему объёму наших данных, то мы сможем выполнять одну операцию ввода/вывода в секунду на каждые 2 ТБ данных, записанных на диске.

В распоряжении S3 пока нет дисков по 200 ТБ, но могу сказать, что мы собираемся их попробовать, как только они появятся в доступе. А также все прочие «номиналы» дисковой ёмкости, которые успеют появиться раньше.

Терморегуляция: размещение данных и производительность

Итак, учитывая всё вышесказанное, отмечу: самые крупные и интересные попадавшиеся мне технические проблемы, связанные с масштабом связаны с уравновешиванием и прочим обслуживанием спроса на ввод/вывод в пределах очень обширного парка жёстких дисков. Мы в S3 называем эту проблему «терморегуляцией» (heat management).

Здесь под «теплотой» понимается количество запросов, попадающих на конкретный диск в некоторый момент времени. Если в данном контексте плохо организовать терморегуляцию, то непропорционально много запросов свалится на отдельно взятый диск, и у нас возникнут точки перегрева. Дело в том, что каждый конкретный диск может выдать лишь ограниченное количество операций ввода/вывода. Нам особенно непросто обеспечить при размещении данных такую оптимизацию, которая позволила бы минимизировать количество точек перегрева на всех наших дисках.

Точки перегрева – это небольшие группы перегруженных дисков, из-за которых замедляется вся система, и ухудшается общая производительность при обслуживании запросов, завязанных на эти диски. Когда вы попадаете в точку перегрева, работа не останавливается, но приходится направлять запросы окольным путём, и пользователь испытывает заметные неудобства. При несбалансированной нагрузке стопорятся те запросы, которые ожидают очереди на обработку на перегруженных дисках, что дополнительно усугубляется зависимыми от них операциями ввода/вывода, груз которых растёт от уровня к уровню. Эти зависимые операции связаны, например, с поиском метаданных или стирающее кодирование (erasure coding). В результате очень невелика получается пропорция тех запросов с особенно сильной задержкой – так называемых «шатунов» (stragglers). Иными словами, точки перегрева на отдельных жёстких дисков порождают хвост в распределении задержек. В конечном итоге, если не обуздать их, то этот хвост вырастет и увеличит задержку у всех запросов.

По мере масштабирования S3 мы стремимся максимально ровно распределить «температуру», чтобы каждый из пользователей мог максимально эффективно работать с HDD из нашего парка. Это непросто, поскольку мы не знаем, когда и как именно пойдут обращения к данным в момент записи, а именно в момент записи приходится решать, где расположить новые данные. Прежде, чем перейти в Amazon, я достаточно долго исследовал и строил системы, призванные прогнозировать такую «температуру» ввода/вывода и управлять ею, но делал это в гораздо более мелких масштабах. Я имел дело с жёсткими дисками на локальных машинах или с корпоративными массивами дисков. В принципе, было практически невозможно добиться в этом высоких результатов. Но в случае с Amazon чистый масштаб несопоставимо больше, а свойственная S3 многоарендность приводит к тому, что мы имеем дело с принципиально иной системой.

Чем больше рабочих нагрузок эксплуатируется на S3, тем хуже корреляция между отдельными запросами, направленными к объектам. Эпизодические нагрузки на хранилища данных обычно возникают скачкообразно. Фактически, большую часть времени основной массив рабочих нагрузок, связанных с хранением данных, просто работает вхолостую, а время от времени испытывают всплески обращений к хранимым данным. В такие пиковые моменты требуется гораздо больше мощностей, чем в среднем. Но, стоит агрегировать миллионы рабочих нагрузок – и происходит по-настоящему крутая вещь: совокупная потребность в мощностях сглаживается и становится гораздо более предсказуемой. Фактически (это наблюдение я сделал во многом интуитивно, перейдя к работе в больших масштабах), как только агрегация достигнет определённого уровня, на котором любая конкретная рабочая нагрузка никак (или почти никак) не влияет на общую величину пика! Итак, когда общее распределение запросов выравнивается при достижении некоторого высокого уровня агрегации, нам остаётся всего лишь взять эти относительно медленные темпы изменения запросов и транслировать их в такое же ровное распределение по всем дискам, достигнув некоторой «средней температуры по хранилищу» для всех рабочих нагрузок.

Репликация: размещение и долговечность данных

В системах хранения данных обычно используются схемы избыточности, призванные защитить информацию при аппаратных отказах, но избыточность помогает и при терморегуляции. Схемы избыточности позволяют размазать нагрузку и направлять трафик запросов так, чтобы уводить его от точек перегрева. В качестве примера рассмотрим репликацию как простой подход к кодированию и защите данных. Репликация позволяет защитить данные при отказе оборудования очень просто: у нас есть множество копий этих данных на разных дисках. Но эта схема также развязывает нам руки, позволяя считывать данные с любых дисков. Размышляя о репликации с точки зрения мощности, признаем, что репликация – дорогое удовольствие. Но с точки зрения ввода/вывода – как минимум, при считывании данных – репликация очень эффективна.

Очевидно, мы не хотим нести издержки за репликацию всех данных, которые у нас хранятся, поэтому в S3 применяется и стирающее кодирование. Например, при помощи такого алгоритма как Рид-Соломон разбиваем наш объект на k «индивидуальных» шардов. Затем генерируем ещё один набор шардов, обладающих m-чётностью. Пока k шардов из общего числа (k+m) остаются доступны, объект поддаётся считыванию. Такой подход позволяет сократить издержки на поддержание мощности, в то же время выдерживая не меньше отказов, чем ранее.

Как масштаб влияет на стратегию размещения данных

Итак, схемы избыточности позволяют нам дробить данные ещё мельче, чем требуется для доступа на считывание. Это, в свою очередь, обеспечивает нам дополнительную гибкость и позволяет не отправлять запросы на перегруженные диски. Но это ещё не всё, что можно сделать для терморегуляции. Следующий шаг – максимально широко размазывать новые объекты по всему парку наших дисков. Тогда как отдельные объекты могут быть закодированы на десятках дисков, мы намеренно размещаем разнородные объекты в разных группах дисков, так, чтобы запросы каждого пользователя были распределены по очень многим дискам.

Мы сильно выигрываем в двух отношениях, распределяя объекты из каждой конкретной категории на много-много дисков:

1. На каждом диске пользовательские данные занимают очень небольшую долю пространства, что позволяет изолировать рабочие нагрузки; дело в том, что конкретная рабочая нагрузка в таком случае не может создать точку перегрева ни на одном диске.

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

Рассмотрим, например, вышеприведённую диаграмму. Этот всплеск может означать, что какой-то клиент занялся геномикой и прямо сейчас параллельно анализирует тысячи лямбда-функций одновременно. Такой всплеск запросов можно обслужить с миллиона отдельных дисков. Я не преувеличиваю. Сегодня у нас десятки тысяч пользователей, чьи корзины S3 распределены более чем на миллион отдельных дисков. Когда я только начинал иметь дело с S3, меня реально восхитила (и научила не хватать звёзд с неба) работа со столь масштабными хранилищами данных. Но, как только я стал понемногу понимать систему, я осознал, что именно имеющиеся масштабы пользовательской аудитории и рабочих нагрузок, обслуживаемых в системе, позволяют выстраивать её по-особенному. При построении систем такого масштаба требуется знать, как резко нарастить производительность до таких величин, которые были бы просто неприменимы на меньших нагрузках.

Человеческий фактор

Сверх технологического фактора значительную роль при эксплуатации S3 играет и человеческий – впрочем, это можно сказать о любой сложной системе. Один из ключевых постулатов Amazon: мы стремимся, чтобы и разработчики, и целые команды умели быстро и безопасно проваливаться (принцип «fail fast»). Они всегда должны быстро и уверенно двигаться при построении систем, в то же время оставаясь абсолютно ориентированы на обеспечение долговечного и надёжного хранения. Чтобы с этим помочь, в S3 разработан процесс под названием «durability reviews» (контроль долговечности). Это аспект человеческого фактора не учитывается в традиционной статистике, но, тем не менее, он очень важен.

Когда инженер вносит изменения, которые могут как-то повлиять на долговечность системы, мы проводим раунд такого контроля. Идея этого процесса позаимствована из исследования безопасности, а именно из моделирования угроз. Цель – резюмировать суть изменения, вывести полный список возникающих угроз, а затем описать, как при таком изменении предполагается их купировать. В области безопасности, расписывая таким образом модель угроз, вы вынуждены мыслить как злоумышленник и представлять все те гнусные вещи, которые можно учинить в вашей системе. При контроле долговечности прививается именно такое мышление «а что может пойти не так?», а сами разработчики учатся рассматривать свой код творчески и, в то же время, критически. Этот процесс очень хорошо ставит две вещи:  

1. Стимулирует авторов и рецензентов по-настоящему внимательно продумывать те риски, от которых следует защититься.

2. Отделяет риски от контрмер и позволяет отдельно обсуждать обе эти стороны вопроса.

При проработке раунда контроля долговечности берём модель угроз, а затем оцениваем, есть ли у нас в запасе адекватные контрмеры и предусмотрены ли варианты защиты. Выявляя эти варианты, мы уделяем особое внимание поиску «лееров», хотя бы в самом общем виде. Эти простые подходы помогают защититься от большого класса рисков. Нам не приходится распутывать каждый отдельный риск и продумывать, как бы его снизить; вместо этого мы пользуемся простыми и широкими стратегиями, обеспечивающими нам комплексную защиту.

Другой пример такой широкой защиты рассмотрим на проекте, который мы начали пару лет назад. Суть его в переписывании самого нижнего уровня хранилища данных в стеке S3 – той части, которая управляет данными на каждом отдельном диске. Новый уровень хранения данных называется ShardStore. Когда мы решили пересобрать этот уровень с нуля, мы натянули для себя, в частности, такой «леер»: взять на вооружение очень интересный набор технологий, который называется «легковесная формальная верификация». Мы с командой решили делать новую реализацию на Rust, чтобы рассчитывать на безопасность типов и структурированную поддержку на уровне языка. Это помогает быстро выявлять баги и даже писать библиотеки, распространяющие эту безопасность типов прямо на те структуры данных, что существуют на диске. С точки зрения верификации мы выстроили упрощённую модель логики ShardStore (также на Rust) и положили её в тот же репозиторий, где уже находилась реализация ShardStore, непосредственно используемая в продакшене. Такая модель позволила избавиться от всей сложности, присущей конкретным слоям данных в дисковом хранилище и самим жёстким дискам, а на практике стала компактной спецификацией. Которой удобно пользоваться. По размеру она сравнима с 1% от объёма реальной системы, но позволяет выйти на такой уровень тестирования, который иначе был бы совершенно неосуществим на жёстком диске со 120 имеющимися IOPS. Мы даже умудрились опубликовать об этой работе научную статью в SOSP.

Оттолкнувшись от этого материала, мы смогли (создавая нужные инструменты и пользуясь уже имеющимися приёмами, например, тестированием на основе свойств) генерировать такие тестовые кейсы, на которых было удобно проверять, совпадают ли динамические свойства нашей реализации с указанными в спецификации. Самая изюминка этой работы не была связана ни, собственно, с проектированием ShardStore, ни с приёмами формальной верификации. Нам больше всего понравилось, что мы смогли, так сказать, «индустриализировать» верификацию, проверяя корректность программы при помощи очень крутых, но слегка академичных приёмов. Мы ввели их в код и добились того, что обычные разработчики, не имеющие PhD в области формальной верификации, теперь могут на равных участвовать в поддержке этой спецификации, а мы – и далее применять наш инструментарий с абсолютно всеми последующими коммитами. Применяя верификацию в качестве леера, наша команда обрела уверенность и смогла ускорить разработку, и эта практика сохранилась, даже когда команда существенно обновилась.

Контроль долговечности и легковесная формальная верификация – два таких примера, которые помогают представить S3 с поистине человеческой, организационной точки зрения. Сама работа по созданию инструментов формальной верификации и внедрению их в работу – сугубо техническая, но занялись мы ею, прежде всего, из стремления помочь коллегам работать быстрее и не терять уверенности даже в условиях постоянного роста и усложнения системы. Аналогично, контроль долговечности помогает команде структурированно подходить к организации этой долговечности, всегда быть ответственными за соблюдение той высокой планки, которую мы здесь себе задали. Можно привести ещё много примеров, демонстрирующих подобное взаимовлияние организации и систем, и интересно видеть, как, уже после такого перехода, остаётся место для экспериментов и инноваций.