Фундамент отказоустойчивых распределенных систем

Бакалавриат 2026/2027

ID 1271923

Статус: Курс по выбору (Прикладная математика и информатика)

Кто читает: Департамент больших данных и информационного поиска

Где читается: Факультет компьютерных наук

Когда читается: 4-й курс, 1, 2 модуль

Охват аудитории: для своего кампуса

Язык: русский

Кредиты: 5

Контактные часы: 84

Дополнительные материалы в LMS Задать вопрос

Аннотация

Курс продолжает базовый курс по распределённым системам и посвящён проектированию, реализации и проверке отказоустойчивых хранилищ. Студенты переходят от линеаризуемого регистра и кворумов к консенсусу, репликации конечного автомата, реконфигурации, шардированию и распределённым транзакциям. Практика состоит из пяти связанных заданий на Python во фреймворке AnySystem; реализации проверяются обычными тестами, симуляцией отказов и model checking. В курс также входят TLA+, storage engines, Chain Replication/CRAQ, CRDT, Spanner, Calvin и основы византийской отказоустойчивости.

Цель освоения дисциплины

Формально различать модели согласованности и проверять линеаризуемость историй.
Проектировать кворумные протоколы и рассуждать об их safety и liveness.
Понимать FLP, детекторы отказов и роль частичной синхронности.
Реализовывать Paxos/Multi-Paxos и Raft, включая репликацию лога и восстановление.
Использовать State Machine Replication для построения сервисов.
Проектировать реконфигурацию и миграцию шардов без потери линеаризуемости.
Понимать LSM- и B+-tree-хранилища, WAL и crash consistency.
Реализовывать 2PC, MVCC и Snapshot Isolation.
Реализовывать 2PC, MVCC и Snapshot Isolation.
Специфицировать небольшой протокол на TLA+/PlusCal и проверять его с помощью TLC.

Планируемые результаты обучения

Студенты смогут реализовывать и отлаживать нетривиальные распределённые протоколы на Python
Студенты смогут моделировать потери сообщений, переупорядочивание, разделение сети, отказы и восстановление узлов
Студенты смогут находить редкие ошибки с помощью симуляции и model checking
Студенты смогут объяснять инварианты и точки линеаризации
Студенты смогут выбирать модель согласованности, схему репликации и механизм транзакций под заданную нагрузку
Студенты смогут анализировать компромиссы между согласованностью, доступностью, задержкой и стоимостью хранения

Содержание учебной дисциплины

Мост и основы корректности
Регистр и кворумы
Broadcast, SMR и консенсус
FLP и CASPaxos
Paxos
Raft и production-консенсус
Спецификация и верификация
Storage engines
Файловые и KV-системы масштаба
Продвинутая репликация
Транзакции и изоляция
Spanner
Calvin и eventual consistency
Византийская устойчивость

Элементы контроля

Домашнее задание 1
Линеаризуемый регистр ABD: read/write-кворумы и majority-репликация. Выдаётся на неделе 1, сдаётся на неделе 3.
Домашнее задание 2
SMR-лог поверх Paxos/Multi-Paxos, дуэль пропозеров и дедупликация. Выдаётся на неделе 3, сдаётся на неделе 6.
Домашнее задание 3
Raft: выбор лидера, heartbeats, репликация лога, persistence и восстановление. Выдаётся на неделе 6, сдаётся на неделе 9.
Домашнее задание 4
Шардированный KV: репликационные группы, config service и online-миграция шардов. Выдаётся на неделе 9, сдаётся на неделе 12.
Домашнее задание 5
2PC поверх ДЗ 4, MVCC-снимки, Snapshot Isolation и конфликты. Выдаётся на неделе 12, сдаётся на неделе 14.
Бонусное задание
На выбор: CRDT-хранилище с G-Counter/OR-Set и anti-entropy либо TLA+-спецификация своего протокола с TLC. Сдаётся на неделе 15.
Экзамен
Устно в аудитории, 120 минут: определения, трассы, доказательство/контрпример и проектирование протокола. Разрешён один двусторонний лист A4; электронные устройства запрещены.

Промежуточная аттестация

2026/2027 2nd module
Итог = Округление(0,70 × ДЗ + 0,30 × Э), где Э — оценка за экзамен ДЗ = 0,15 × ДЗ1 + 0,20 × ДЗ2 + 0,25 × ДЗ3 + 0,20 × ДЗ4 + 0,20 × ДЗ5, где каждая работа оценена по шкале 0–10

Программа дисциплины