Книга: UNIX: A history and a Memoir

После мюнхенских курсов по системному програмированию во мне опять проснулась тяга к Unix-археологии. Выразилось это в покупке книги Брайана Кернигана — «UNIX: A History and a Memoir».

Заслуги Кернигана перечислять можно долго, но, конечно, главной из них стало участие в разработке оригинальнальных Unix в знаменитой Bell Labs. Почти все мои любимые инструменты — программы, языки программирования, утилиты — они все родились где-то в тех краях. Операционная же система, что использую ежедневно еще с 90-х — клон той же самой ОС, которой посвящена книга.

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

И последнее мне особенно было интересно. Какие люди делают такие вещи? Какая организация может собрать множество такого калибра талантов под одной крышей? Какой руководитель дал им возможность работать над этими проектами?

Какой-то технической информации в книге мало, и только в количестве необходимом для рассказала об эволюции Unix. Ответы на технические вопросы стоило бы поискать в другой книге.

Да, эта книга совершенно точно стоит своих денег, и дело не только в Unix.

Книга: Database Internals

Базы данных — тема интересная, старая и разносторонняя. И удивительно, что литературы по устройству баз данных не так много. Известные мне книги либо ограничиваются сугубо теоретическими вопросами, либо рассматривают БД с точки зрения программиста-пользователя.

И известные мне классические книги излагают именно традиционный подход к базам данных, когда хранилище целиком умещается на единственную большую машину, и нет никаких серьезных проблем, характерных для распределенных систем.

Поэтому я старательно отслеживаю все новые публикации на тему, и мимо книги с названием «Database Internals: A Deep Dive into How Distributed Data Systems Work» пройти никак не мог.

Впечатления о книге…

Меня преследует TLA+

Подписан я на блог-рассылкуThe Morning Paper, автор которой разбирает интересные классические или новые научные публикации на околоайтишные темы: распределенные системы, языки программирования, базы данных и так далее.

Пару дней назад «Утренняя работа» предложила обсудить некую работу. Статья обсуждает, безусловно, интересные и актуальные вещи, но мое внимание привлекло то, что исследователи из Amazon опять упоминают TLA+ — язык формальной спецификации систем и идущая комплектом программа-верификатор.

Словом, прочитал несколько вводных статей и попробовал написать пару простеньких спецификацию.

Выяснилось, что TLA+ и компилируемый в него PlusCal позволяют описать систему и проверить ее на предмет соответствия каким-то требованиям или инвариантам. Тут все вкусно, питательно и полезно.

Но почему все так ужасно с точки зрения эргономики программиста?!

Во-первых, почему оно работает только через какую-то дубовую среду разработки (TLA Toolbox)?! Причем среда-то не особо помогает, но зато прячет обычные консольные программы.

Во-вторых, реализация дуализма TLA+/PlusCal. Ну ладно, что там два языка (читаемый PlusCal компилируется в нечитаемый TLA+). Но кому пришла в голову мысль о том, что PlusCal пишется прямо в комментариях TLA? И код этот ракрывается на лету интегрированной средой?! Прямо Java образца 2005 года, с ее адскими генераторами XML.

В-третьих, кому (тому самому Лэсли Лампорту, на секундочку) пришла в голову мысль о двух синтаксисах в PlusCal?! TLA и PlusCal и так довольно мусорные языки, а тут еще и разнобой стилевой.

Да что это я распинаюсь? Судите сами! Пример (простой):

---- MODULE transfer ----
EXTENDS Naturals, TLC

(* --algorithm transfer
variables alice_account = 10, bob_account = 10,
          account_total = alice_account + bob_account;

process Transfer \in 1..2
  variable money \in 1..20;
begin
Transfer:
  if alice_account >= money then
    A: alice_account := alice_account - money;
        bob_account := bob_account + money;
end if;
C: assert alice_account >= 0;

end process

end algorithm *)
\* BEGIN TRANSLATION
\* Label Transfer of process Transfer at line 12 col 3 changed to Transfer_
VARIABLES alice_account, bob_account, account_total, pc, money

vars == << alice_account, bob_account, account_total, pc, money >>

ProcSet == (1..2)

Init == (* Global variables *)
        /\ alice_account = 10
        /\ bob_account = 10
        /\ account_total = alice_account + bob_account
        (* Process Transfer *)
        /\ money \in [1..2 -> 1..20]
        /\ pc = [self \in ProcSet |-> "Transfer_"]

Transfer_(self) == /\ pc[self] = "Transfer_"
                   /\ IF alice_account >= money[self]
                         THEN /\ pc' = [pc EXCEPT ![self] = "A"]
                         ELSE /\ pc' = [pc EXCEPT ![self] = "C"]
                   /\ UNCHANGED << alice_account, bob_account, account_total,
                                   money >>

A(self) == /\ pc[self] = "A"
           /\ alice_account' = alice_account - money[self]
           /\ bob_account' = bob_account + money[self]
           /\ pc' = [pc EXCEPT ![self] = "C"]
           /\ UNCHANGED << account_total, money >>

C(self) == /\ pc[self] = "C"
           /\ Assert(alice_account >= 0,
                     "Failure of assertion at line 16, column 4.")
           /\ pc' = [pc EXCEPT ![self] = "Done"]
           /\ UNCHANGED << alice_account, bob_account, account_total, money >>

Transfer(self) == Transfer_(self) \/ A(self) \/ C(self)

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == (\E self \in 1..2: Transfer(self))
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

MoneyNotNegative == money >= 0
MoneyInvariant == alice_account + bob_account = account_total

====

Уф… А книжку по языку все равно придется почитать.

Все, что надо знать об истории UNIX

There are no locks in the file system, nor is there any restriction on the number of users who may have a file open for reading or writing. Although one may imagine sutations in which this fact is unfortunate, in practice difficulties are quite rare.

— Denis Ritchie, draft of the The UNIX Time-Sharing System manual

История UNIX и связанных с ним инструментов — моя слабость. Особенно интересно бывает разбирать происхождение каких-нибудь совершенно бытовых вещей, вроде утилит cat, crontab или классических системных вызовов.

На выходных совершенно случайно открыл для себя cat-v. org, сборник ссылок и документов, непосредственно или косвенно связанных с Bell Labs, откуда вышли UNIX, языка C, awk, sed и тысячи других утилит, составляющих основу моего профессионального мира.

Помимо руководств (англ. man) к ключевым версиям версии Unix там есть совершенно потрясающие документы вроде черновика самого первого руководства, написанного еще до появления Unix внутри Bell Labs. Рекомендую ознакомиться — основы Linux не сильно изменились по сравнению с Unix от 1971 года!

Ну и всякие другие вкусности: введение в использование первых публичных версий Unix (Version 6 Unix и Version 7 Unix), история Unix от современников и много другое.

PS Ах, да, кстати, про UNIX и Linux. Оказывается, в документации Linux существует описание структуры дерева файловой системы. Революция сознания!

Идиомы использования макросов в Лиспах

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

Соответствующий механизм здесь называется макросами. Макросы это функция, получающая на вход код структуры данных, и меняющая ее по своему усмотрению, и возвращающая видоизмененный код (тоже как структуру данных). После выполнения (раскрытия) макроса интерпретатор исполнит получившийся код:

(defmacro evaluate-left-only (left-form right-form)
    left-form)
(evaluate-left-only (print t) (print nil))
;;;; evaluating (print t)
;; => t

В примере мы ввели два макроса. Макрос (evaluate-left-only) передает, не меняя, интерпретатору свой левый аргумент (left-form), который и вычисляется, выводя t.

Другими словами, макросы — мощнейший инструмент, позволяющий программисту менять смысл (семантику) выражений языка по своему усмотрению. В сущности, богатые на макросы программы превращаются в специализированные мини-языки, затрудняющие чтение кода незнакомыми с кодом разработчиками.

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

Немного прикладной макрологии…

Книга: Semantics with Applications

Мои познания о формальном подходе к семантике языков програмирования в лучшем случае поверхностны, но повода их углубить, в общем-то, до сих пор не было. Но тут попалась вводная книга по семантике языков программирования: Semantics with Applications.

Впечатления о книге…

Статья: ORBIT: An Optimizing Compiler for Scheme

Мир традиционных Лиспов делится на два больших семейства: родственники Common Lisp и многочисленные реализации Scheme. Common Lisp был разработан соответствующим комитетом как компромисс между многочисленными промышленными Лиспами 70-х и 80-х. И, как типичный управляемый комитетом стандарт, ANSI Common Lisp страдает многословностью и противоречивостью, что выражается в тысяче с лишним страниц определения языка.

Стандарты базовой Схемы занимают каждый порядка сотни страниц, определяя простое и легкое в реализации и понимании ядро языка. Но есть проблема: стандарт не очень практичен, и не включает в себя скучные частные вопросы. Ну, вроде стандартной библиотеки для работы с регулярными выражениями…

Тем не менее, лаконичность и простота Схемы привела к тому, что в среде академиков и энтузиастов создание эффективных интерпретаторов и компиляторов Схемы стало чем-то вроде спорта: мелких реализаций разве что не сотни, крупных — десятки. В них обкатываются новые техники компиляции функциональных и динамических языков, проверяются подходы к проблемам отрасли и просто развлекаются скучающие программисты.

Первая экспериментальная реализация компилятора Scheme была описана Гаем Стилом (англ. Guy Steele еще в конце семидесятых (см. публикацию Rabbit: A Compiler for Scheme, 1978 год). Но первым практичным компилятором стал Orbit, ключевая работа по которому была опубликована только в 1986 году.

Orbit оказал огромное влияние на все последующие компиляторы функциональных языков, в том числе Haskell, SML/NJ и многие другие, поэтому знакомство показалось мне обязательным. Во время двухдневного полета в Мюнхен у меня нашлось (много!) времени на чтение той самой первой публикации (ORBIT: An Optimizing Compiler for Scheme, длиной в 16 страниц), и получившиеся заметки хотелось бы сохранить в блоге.

Выход на Orbit-у

Курсы по системному программированию с Майклом Керриском

Всю прошлую неделю я провел в Мюнхене, на интереснейших курсах по системному программированию под Линуксом (Linux/UNIX System programming).

Приключение это далось непросто: надо было убедить начальство (Артем, огромное спасибо!) профинансировать в индивидуальном порядке недешевые занятия и поездку; дождаться самих курсов, до последнего момента остававшихся под вопросом; и, наконец, преодолеть жуткий ураган, из-за которого перелет из Лондона в Мюнхен занял два дня (вместо полутора часов). Удалось даже встретиться со старыми друзьями, с которыми довелось работать над большими вьетнамским поиском (спасибо за теплый прием, Саша!).

/images/system-programming-study.jpg

И оно стоило того. …

Книга: Compiling with Continuations

В последние годы я почти совсем перестал читать художественную литературу, а все любимые книги посвящены если не околопрофессиональным, то как минимум околонаучным темам. Со временем я обнаружил, что и в технических публикациях встречаются по-литературному талантливые авторы, легко излагающие самые сложные темы.

Один из таких выдающихся авторов — Эндрю Аппель, специалист по компиляторам в целом и компиляторам функциональных языков в частности. Его книги и ключевые научные публикации по качеству прозы — и красоте идей! — можно сравнить только с интересным романом. Книгу Modern Compiler Implementation in ML («тигровую книгу», по обложке), например, я читал раза три и, вероятно, еще не раз к ней вернусь.

Но Аппель прославился не только популярным учебником. Другая его книга, Compiling with Continuations, популяризовала и сделала стандартом в мире компиляторов функциональных языков внутреннее представление в стиле передачи продолжений (англ. continuation passing style). Ее я читал и перечитывал в последние недели.

О классике…