Пользователь
Продолжаем серию статей о CAP-теореме и языке Coq. В предыдущей части мы детально проанализировали определения CAP-теоремы, готовясь к её формализации на языке Coq, и нашли там серьёзную ошибку (теперь будет о чём поговорить при случае на system design interview).
В этой статье мы познакомимся с основами языка Coq и для практики формализуем небольшой фрагмент геометрической системы, близкой к евклидовой.
No subject appears to be more controversial to distributed systems engineers than the oft-quoted, oft-misunderstood CAP theorem. The CAP FAQ
— Сейчас я тебе объясню... — Объяснить я и сам могу, ты расскажи, что на самом деле происходит! (Из разговора политологов, но для CAP-теоремы подходит тоже)
— Давайте уже запишем CAP-теорему на языке Coq и посмотрим, что там на самом деле. (Я)
В Go есть возможность получить отчёт о выполняемом escape-анализе: go build -gcflags '-m=3 -l'. В этой статье я расскажу, как можно визуализировать этот отчёт в VS Code. Дополнительно приведу способ, как в несколько кликов проверить теорию (escape-анализ) практикой (профилирование).
Участвую в стартапе, в котором разрабатывается СУБД нового типа (работает поверх некоторых kv-движков, кардинально расширяя их возможности, про это немного можно прочитать здесь). Для того, чтобы сравнить то, что понемногу получается, с тем, что имеется в индустрии, пришлось на глубоком уровне проработать первоисточники по темам Isolation и Consistency (уточню, что имеется ввиду не та Consistency, что в ACID). Обнаружил интересные нюансы, которые и излагаю в этой статье.
Тезисно:
Ну, и ещё кое-что по мелочи. В конце рассмотрим вот такой венец творения человеческого разума:
В статье Наблюдение за выполнением конкурирующих задач в Go и Rust коллега cpmonster привёл весьма интересные результаты:
Программа на Rust показала намного большую производительность при вычислении членов возвратной последовательности, чем программа на Go: 367 млн. итераций в секунду против 44 млн.
Ну, в 1.5 раза… Ну, в 2 раза… Но семь гвардейцев за два дня? — это слишком, тем более что тут "гвардейцев" больше восьми!
Или нет, не слишком? В общем, потенциал любопытства пересилил другие потенциалы и я провёл своё исследование.
Вторая часть про работу с кучей, устанавливаем свой глобальный аллокатор. В принципе, это делается в несколько строк, но наша цель — действовать сознательно и профессионально, с глубоким проникновением в суть явлений, так что легкой жизни не будет (как и обещал).
Продолжаем изучать Rust нетрадиционным способом. В этом раз будем разбираться в нюансах работы с кучей, для их понимания понадобятся: сырые указатели, выделение памяти в куче, размер экземпляра типа, запись значений в кучу и чтение из нее, const и static, unit-like структуры, переопределение глобального аллокатора.
Это, определенно, overkill для одной статьи, а вот половину списка вполне можно освоить.
Продолжаем работать с 10.3.
КМБ.- Двойная жизнь.- Восстание мертвецов.- Ошибка в документации.- Ужасающие подробности из The Rustonomicon.- Архитектурные озарения.- Развязка.
После главы 4 (было здесь) переходим к 10.3. Валидация ссылок при помощи времён жизни. Ну а куда еще… такие нынче времена.
Перед вами краткое профессиональное описание особенностей языка Rust для профессионалов.
Чего здесь НЕ будет
Северная столица в плане погодных условий вполне пригодна для поездок на велосипеде в зимний период. Но предварительно нужно победить дракона, прогнать жабу и еще понадобятся две волшебные спички.
В начале этого года я прочитал на habr любопытную статью "Почему Discord переходит с Go на Rust", переход был связан с неэффективным механизмом сборки мусора в Go. Тогда подумалось, что, наверное, было бы проще доработать приложение и не переходить. Но еще проще было бы избежать таких проблем на стадии разработки.
Подумав хорошенько, я решил, что справлюсь с этим делом. Тогда я пошел и купил бутыль свинцовой примочки и велосипед. Домой меня провожал инструктор, чтобы преподать мне начальные сведения. Мы уединились на заднем дворе и принялись за дело.
Марк Твен. Укрощение велосипеда
