вторник, октября 19, 2010

Haskell monads для физматовца. Краткое введение

Ну что, попробую пополнить ряды haskell newbies ;)

Я не уверен, что данная заметка сделает концепцию монад понятнее для профессиональных программистов на чём-нибудь типа Java. Но я надеюсь, что она поможет людям с некоторым математическим бэкграундом. Но даже им, думаю, эта заметка поможет в практическом программировании только в сочетании с другими monad tutorials.

АФАИК, во многих наших провинциальных вузах на физмат-специальностях теория категорий (вместе с современной теорией множеств) игнорируется полностью (т.е. о её существовании за 4-5-6 лет ни разу не упоминают даже, как это было у меня). Я не собираюсь излагать всю теорию — кому нужно, смотрите книжки или хотя бы википедию. Я изложу только то, что нужно для нашего применения.

Категории

Итак. Вводится понятие категории. Это некая очень абстрактная сущность (абстрактнее даже, чем множество). В некотором смысле, категория состоит из двух вещей: набора объектов и набора морфизмов. Относительно этих объектов и морфизмов выполняются какие-то там аксиомы. Из них следует, что категорию можно представлять в виде направленного графа, где вершины — это объекты категори, а дуги — это морфизмы категории. Существенно, что у морфизма, как у дуги графа, есть «начало» и «конец» (называемые домен и кодомен), и это объекты той же категории. Домен и кодомен морфизма (начало и конец дуги графа) могут совпадать. Такой морфизм называется эндоморфизмом.

Классический пример категории — Set. Объекты категории Set — это всевозможные множества, а морфизмы — это функции между этими множествами.

Более интересный для нас пример: категория Hask. Здесь объекты — это типы данных, возможные в языке Haskell, а морфизмы — функции языка Haskell.

Функторы

Следующее понятие: функтор. Функтор — это, условно говоря, отображение одной категории в другую. При этом функтор отображает объекты первой категории в объекты второй, а морфизмы первой — в морфизмы второй категории. К тому же накладываются определённые ограничения — аксиомы.

Если функтор отображает категорию саму в себя, такой функтор называется эндофунктором.

Возьмём нашу категорию Hask. Любой полиморфный тип данных языка Haskell с одним тИповым аргументом задаёт отображение, сопоставляющему каждому объекту категории Hask (т.е. типу языка Haskell) какой-то другой объект (другой тип). Например, конструктор типов [] сопоставляет любому типу a тип [a] (список элементов типа a). Конструктор типов Maybe сопоставляет каждому типу a другой тип — Maybe a (значение типа a или никакого значения). Таким образом, мы можем привести много примеров отображений класса объектов категории Hask в объекты той же категории. Пусть, например, у нас есть конструктор типов C (т.е. где-то написано data C a = …).

Если теперь такое отображение объектов (конструктор типов C с одним параметром) дополнить отображением морфизмов, то получим функтор, действующий из Hask в Hask (говорят «эндофунктор на категории Hask»). Напомню, морфизм категории Hask между объектами (типами) a и b — это любая функция типа a → b. Согласно аксиомам функторов, морфизм между объектами a и b должен отображаться в морфизм между объектами (C a) и (C b). Таким образом, отображение морфизмов должно быть функцией следующего вида:

    fmap :: (a -> b) -> (C a -> C b)

В модуле Prelude определён класс типов Functor:

    class Functor f where
fmap :: (a -> b) -> (f a -> f b)

Итак, любой тип, являющийся экземпляром класса Functor, является эндофунктором на категории Hask (т.е., название класса Functor не вполне точное, его бы следовало назвать, скажем, HaskEndoFunctor). При этом сам конструктор типов задаёт отображение объектов (типов), а связанная с ним функция fmap задаёт отображение морфизмов (функций).

Моноиды

Моноид — это термин несколько из другой (хоть и смежной) области — из абстрактной алгебры. Моноид определяется следующими вещами:

  • Множество M;

  • Бинарная операция ⊕ на этом множестве; от неё требуется ассоциативность;

  • Нейтральный элемент ε этой операции, входящий в множество (т.е. такой, что (∀a ∈ M) ε⊕a = a⊕ε = a).

Можно видеть, что моноид — это ослабление понятия группы. Благодаря этому, очень многие структуры являются моноидами. Ну, скажем, множество действительных чисел с операцией сложения. Или множество списков элементов какого-то одного типа с операцией (++).

Монады

Ну а теперь главное определение ;). Монада — это моноид в категории эндофункторов. Расшифровываю.

Пусть у нас есть какой-нибудь эндофунктор на категории Hask (т.е. тип f, являющийся экземпляром класса Functor). Дополним его структурой моноида. Для этого нам понадобится бинарная операция и её единичный элемент. Подходящая бинарная операция традиционно называется bind (и в haskell обозначается >>=). Подходящий единичный элемент традиционно называется return. В Haskell это выражается в следующее определение:

    class Monad m where
(>>=) :: m a -> (a -> m b) -> m b -- бинарная операция
return :: a -> m a -- единичный элемент

В модуле Prelude объявлены экземпляры класса Monad для некоторых типов: [], Maybe, итп.

К чему это я всё

Из всего вышесказанного можно вывести очевидную вещь: монады — очень абстракная сущность. Настолько абстрактная, что чуть ли не всё на свете является монадой.

С другой стороны, это очень простая штука: некий аналог действия «композиция функций», только при композиции используется какая-то дополнительная информация.

вторник, августа 24, 2010

Душа?

Я, кажется, понял, что такое душа :) По крайней мере, с точки зрения кибернетики.

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

  1. Какие лампочки сейчас горят, зависит только от того, какие кнопочки сейчас нажаты, и ни от чего больше.

  2. Включение лампочек зависит не только от того, какие кнопки нажаты, но и от порядка нажатия.

Пусть мы хотим моделировать такие ящики на Haskell. Пусть мы ввели тип X для обозначения множества нажатых в данный момент кнопок, и тип Y — для множества горящих лампочек. Например, это можно сделать так:

import qualified Data.Set as S
type Button = Int
type Lamp = Int
type X = S.Set Button
type Y = S.Set Lamp

Тогда ящик из пункта 1) можно полностью описать функцией с типом

f1 ∷ X -> Y

Это так называемая чистая функция. Заметим, что такая функция не может создавать слишком сложного поведения ящика. Действительно, если f1 очень замысловатая, то, тыкая в кнопки на ящике, мы не сможем разгадать устройства функции f1. Но мы сможем составить табличку из двух колонок: «нажатые кнопочки», «горящие лампочки». Формально говоря, эта таблица — график функции f1. Строк в этой таблице должно быть всего-то навсего 2^10, т.е. 1024. Пользуясь этой таблицей, мы легко сможем предсказывать поведение ящика, сколь бы сложной ни была функция f1.

Ящик же из пункта 2) можно описать функцией с более сложным типом:

import Control.Monad.State
f2 ∷ X -> State St Y

где St — какой-нибудь более или менее замысловатый тип данных. Гипотеза: чем сложнее тип St, тем сложнее может быть поведение функции f2. Возьмём сначала очень простой тип: type St = Bool. Тогда f2 представляет собой конечный автомат с двумя состояниями. Ничего принципиально более сложного, чем двухтактный счётчик, из такого автомата не сделать. Возможно, например, такое поведение: при чётных нажатиях на первую кнопку загорается пятая лампочка, а при нечётных - десятая. Этот алгоритм легко разгадать наблюдениями, никакой загадочности в нём нет. Если type St = Int, то можно придумать уже гораздо более сложное поведение. А уж если, скажем,

data Tree a = Node a | Branch [Tree a]
type St = Tree [Maybe Int]

или что-нибудь ещё такое понавороченнее, то поведение f2 может быть очень сложным и даже загадочным. В процессе нажимания на кнопочки на таком ящике и наблюдения за лампочками нас вполне может посетить мысль, что в ящике сидит какой-то инопланетянин, а кнопочки и лампочки — это у него такой способ общения. Ну, я думаю, вы уже поняли мою гипотезу: душа — это и есть вот это состояние в смысле монады State!

Отсюда следуют некоторые интересные мысли. Например, мы часто говорим о человеке что-нибудь вроде «у него сложный характер» или там «у него настоящая загадочная русская душа»… Оказывается, в указанном выше смысле, понятию сложности души можно придать вполне конкретный смысл — это просто сложность типа данных! :)

Или рассмотрим какую-нибудь очень сложную программу, например банковскую опердень или ОС Windows. Такие программы обладают одновременно двумя свойствами:

  • Их поведение во многих случаях загадочно, далёкие от ИТ пользователи даже часто склонны их одушевлять;

  • Они написаны так, что содержат изменяемое состояние, причём это состояние само по себе очень сложное (ну, например, состояние базы данных).

В свете рассуждений выше мы видим, что одновременность появления этих свойств отнюдь не случайна. «Душа» таких программ по сложности сопоставима с душой человека, что ж удивляться, что она загадочна? Кроме того, оказывается, те далёкие от ИТ пользователи правы в вышеприведённом смысле.

понедельник, августа 02, 2010

Небольшая иллюстрация к предыдущему

Нашёл у Гейтинга [1] иллюстрацию к изоморфизму Карри-Ховарда. Что интересно: насколько я понял, эта иллюстрация была сформулирована до самого изоморфизма.

«Пусть A обозначает свойство натурального числа быть кратным 8, B — быть кратным 4, C — кратным 2. 8a мы можем записать как 4∙2a; благодаря этому математическому построению (P) мы видим, что свойство A влечёт свойство B, или A → B. Подобное построение (Q) показывает, что B → C. Употребляя сначала P, потом Q (суперпозиция P и Q), мы получаем 8a = 2∙(2∙2a), что доказывает A → C. Этот процесс остаётся пригодным, если вместо A, B, C мы подставим произвольные свойства. А именно, если построение P доказывает, что A → B, и построение Q доказывает, что B → C, то суперпозиция P и Q доказывает, что A → C».

Если считать «построения» функциями, то из этого рассуждения увидим, что существование операции суперпозиции двух функций (P и Q) доказывает транзитивность импликации:

(.) :: (b -> c) -> (a -> b) -> a -> c

[1] А. Гейтинг. Введение в интуиционизм. М.: Мир, 1965.

пятница, июля 23, 2010

Вычислимость, λ-исчисление, теория типов, автоматизация доказательств

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

λ-исчисление

λ-исчисление было создано в начале 50-х гг. XX века для формализации понятий вычисления и вычислимости в математике. λ-исчисление оперирует символами и λ-выражениями. Символ — это одиночный абстрактный объект, иногда символы называют переменными. Символы обозначают маленькими латинскими буквами: x,y,z… λ-выражение определяется рекурсивно:

  • Если x — это символ, то x — это λ-выражение;

  • Если x — символ, а E — λ-выражение, то запись λx.E — тоже λ-выражение;

  • Если E — λ-выражение, то (E) — λ-выражение;

  • Если E1 и E2 — λ-выражения, то E1 E2 — тоже λ-выражение.

Выражения вида λx.E называют λ-функциями, или просто функциями. Если в таком выражении символ x встречается в выражении E, он называется связанным. Несвязанные символы, встречающиеся в λ-выражении, называются свободными.

Для любого λ-выражения E можно записать выражение λx.E, где x — свободный символ выражения E (и, таким образом, связать символ x). Эта операция называется λ-абстракцией.

Введём обозначение: записью E[x=T] будем обозначать выражение, полученное из E заменой всех вхождений символа x на T.

Над λ-выражениями можно производить следующие операции:

α-конверсия

E → E[x=y]; т.е. переменные можно переименовывать;

β-редукция

(λx.E1) E2 → E1[x=E2]; это подстановка;

η-редукция

λx.(E x) → E (избавление от лишней абстракции).

Видно, что α-конверсию можно применить к любому выражению, а редукции — только к выражениям определённого вида.

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

Теорема. Если у выражения есть нормальная форма, то она только одна. Любая последовательность редукций приведёт к этой нормальной форме.

Таким образом, выполняется единственность. Но существование выполняется не всегда: не у всех выражений есть нормальная форма.

Example 1: Пример.

ω = (λx.x x) (λx.x x)

ω = (λx.x x) (λy.y y) = (λy.y y) (λy.y y) = (λy.y y) (λz.z z) = (λz.z z) (λz.z z) = …

Последовательность редукций не изменяет это выражение.

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

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

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

Введём обозначение: λx.λy.λz.λ…E будем записывать как λx y z….E.

Натуральные числа.

За 1 примем выражение λx.x. Для каждого «числа» E следующим числом будем считать выражение λx.E. Таким образом, двойке будет соответствовать выражение λx y.y, тройке — λx y z.z, и т.д. Далее определения действий над числами вводятся как в аксиоматике Пеано. Такая запись чисел называется кодировкой Чёрча.

Выражения «если-то».

За логическую истину примем выражение λx y.x, за логическую ложь — λx y.y. Тогда выражение λc x y.c x y будет соответствовать конструкции «if-then-else». Действительно,

  • if TRUE A B = (λc x y.c x y) (λx y.x) A B = (λx y.x) A B = A;

  • if FALSE A B = (λc x y.c x y) (λx y.y) A B = (λx y.y) A B = B. Кроме того, оказывается, что можно ввести и обычные логические действия — and, or и т.д.

Пары (кортежи из двух элементов).

Пусть

pair = λf.λs.λb.b f s
fst = λp.p TRUE
snd = λp.p FALSE

Тогда выражение pair x y создаёт кортеж (x,y), функция fst возвращает первый элемент кортежа, snd — второй. Действительно,

pair x y = λb.b x y;
fst (pair x y) = (λp.p TRUE) (λb.b x y) = (λb.b x y) TRUE = TRUE x y = x;
snd (pair x y) = (λp.p FALSE) (λb.b x y) = (λb.b x y) FALSE = FALSE x y = y.

Кортежи из трёх и более элементов, очевидно, можно составлять из пар, например pair x (pair y z) — кортеж из трёх элементов.

Проблема останова

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

Теорема. Проблема останова в общем случае неразрешима.

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

Теория типов

Введём в λ-исчисление типизацию. Именно, кроме символов и выражений, теперь в теории будут фигурировать типы — тоже абстрактные объекты. Типы будем обозначать маленькими греческими буквами: τ, σ… Любое λ-выражение должно иметь тип, и при том только один. Это записывается как E : τ. Типы определяются также рекурсивно:

  • Если τ — тип, то (τ) — тип;

  • Если τ и σ — типы, то τ → σ — тип.

Типы без стрелок и других операций называются простыми типами. Все символы имеют простые типы.

Тип выражения определяется по следующим правилам:

  • Если x : τ и E : σ, то (λx.E) : τ → σ;

  • Если F : τ → σ и x : τ, то (F x) : σ.

При этом если в выражении F x окажется, что F : τ → σ и x : τ1, причём τ ≠ τ1, то говорят, что выражение неверно типизированное. В типизированном λ-исчислении рассматриваются только верно типизированные выражения.

Тип называется населённым, если существует хотя бы одно λ-выражение, имеющее такой тип.

Example 2: Пример.

Попробуем типизировать выражение λx.x x. Пусть x : τ. Тогда, чтобы к x, стоящему в выражении последним, можно было применить предыдущий x, этот предыдущий x должен иметь тип τ → σ, где σ — какой-то ещё тип. Но (x : τ) и (x : τ → σ) не может выполняться одновременно, т.к. у каждого символа может быть только один тип. Пришли к противоречию. Итак, рассматриваемое выражение неверно типизировано, а значит, неверно типизировано и упомянутое в предыдущем примере выражение ω. Таким образом, оказалось, что невычислимое выражение ω не входит в типизированное λ-исчисление.

Оказывается, что верна следующая

Теорема. Если λ-выражение верно типизировано, то оно вычислимо.

Таким образом, в рамках типизированного λ-исчисления проблема останова решается очень просто: все выразимые в этой системе алгоритмы завершаются.

Неудивительно, что при этом оказывается, что эта система не является тьюринг-полной. Т.е. существуют алгоритмы, которые можно представить в виде программы для машины Тьюринга, но нельзя записать в рамках типизированного λ-исчисления. Из этого можно сделать два замечания:

  • Само по себе типизированное λ-исчисление не несёт большой практической ценности, т.к. не позволяет выразить многие алгоритмы;

  • С другой стороны, т.к. множество типизированных выражений является подмножеством нетипизированных, появляется намёк на решение проблемы останова: чтобы выяснить, вычислимо ли данное выражение, нужно только проверить, является ли оно верно типизированным. Неудивительно, что как раз эта задача (проверить возможность типизации для произвольного выражения) оказывается неразрешимой.

Для возможности практического применения λ-исчисления разработаны системы типов, накладывающие меньше ограничений, чем вышеприведённая. Такие системы:

  • достаточно выразительны, т.к. являются тьюринг-полными;

  • вывод типов в них оказывается разрешимой задачей;

  • но проблема останова, как и в случае нетипизированного λ-исчисления, неразрешима.

На таких "промежуточных" системах типов основаны имеющие практическое применения функциональные языки программирования.

Автоматизация доказательств

Для нужд практического программирования в теории типов обычно добавляют такое правило:

  • Если τ и σ — типы, то τ*σ и τ+σ — тоже типы.

В λ-исчислении можно определить понятие пары (E1,E2) и понятие «одно из двух» E1|E2. При этом оказывается, что:

  • Если E1 : τ, E2 : σ, то (E1,E2) : τ*σ,

  • и E1 | E2 : τ+σ.

Оказывается, что между терминами теории типов и терминами логики высказываний существует естественное соответствие. Именно:

  • Простой тип τ соответствует простому высказыванию;

  • Сумма типов соответствует дизъюнкции;

  • Произведение типов — коньюнкции;

  • Стрелка — импликации.

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

Теорема (изоморфизм Карри-Ховарда). Теорема логики высказываний верна тогда и только тогда, когда соответствующий ей тип населён, т.е. любое λ-выражение, имеющее этот тип, можно рассматривать как доказательство теоремы.

Более сложные, чем вышеприведённая, системы типов позволяют записывать не только теоремы логики высказываний, но и теоремы логики более высоких порядков. При этом изоморфизм Карри-Ховарда остаётся в силе.

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

  • Записать данную теорему в виде типа в одной из систем типов;

  • Найти выражение, населяющее этот тип;

  • Записать это выражение на языке предметной области.

суббота, марта 20, 2010

LiveMath III

Это продолжение к стародавнему посту: http://iportnov.blogspot.com/2007/09/livemath-livecd.html.

К сожалению, редко оказывается достаточно времени, чтобы собрать свежую версию LiveMath. Однако же вот, собрал. В этот раз LiveMath основан на Ubuntu 9.10 (Karmic) с добавлениями из Ubuntu Lucid и "Ubuntu Scientific Remix". LiveMath III содержит (среди прочего):

Системы компьютерной алгебры:
Maxima (http://maxima.sourceforge.net) - полнофункциональная система аналитических вычислений;
Fricas (http://fricas.sourceforge.net) - мощная система компьютерной алгебры;
YaCas (http://yacas.sourceforge.net) - еще одна система компьютерной алгебры;
PARI/GP (http://pari.math.u-bordeaux.fr/) - широко используемая компьютерно-алгебраическая система, разработанная для быстрых вычислений в теории чисел (факторизации, алгебраическая теория чисел, эллиптические кривые...);
GAP (http://www.gap-system.org/) - свободно распространяемый, открытый и расширяемый программный комплекс для применения в области вычислительной дискретной математики, в частности, теории групп;
Mathomatic (http://www.mathomatic.org/) - переносимая, универсальная программа, которая может решать, упрощать, группировать, дифференцировать, интегрировать и сравнивать алгебраические выражения;

Системы автоматизации доказательств:

ACL2 (http://www.cs.utexas.edu/users/moore/acl2/) - язык программирования для моделирования компьютерных систем и средство, помогающее доказывать свойства этих моделей;
Coq (http://coq.inria.fr/) - система автоматизированного построения доказательств, с помощью которой, кроме всего прочего, была решена проблема четырех красок;
Также Prover9/Mace4 и некоторые другие;

Системы численных вычислений:

SciLab (http://www.scilab.org/) - пакет научных программ для численных вычислений, предоставляющий мощное открытое окружение для инженерных и научных расчетов;
GNU Octave (http://www.octave.org/) - язык высокого уровня, предназначенный для выполнения математических вычислений;
FreeMat (http://freemat.sourceforge.net/) - свободная среда для быстрой разработки, научного прототипирования и обработки данных, имеет интерфейс и синтаксис языка, подобные MatLab;
Yorick (http://yorick.sourceforge.net/) - компактная программная среда, предназначенная для комплексного решения научно-инженерных вычислительных задач;

Образовательные программы:
Kig (http://edu.kde.org/kig/), Carmetal, DrGeo, GeoGebra - интерактивная геометрия;
KAlgebra;
Инструменты построения графиков - kmplot, gnuplot;

Обработка и визуализация данных:
Mayavi2 (http://code.enthought.com/projects/mayavi/#Mayavi2) - открытый пакет научной 2D и 3D визуализации данных;
OpenDX (http://www.opendx.org/) - программное средство для анализа данных в графическом виде, визуализации научных данных;
GGobi (http://www.ggobi.org/) - среда визуализации многомерных данных;
LabPlot (http://labplot.sourceforge.net/) - программа для анализа и визуализации различных данных;
QtiPlot - позиционируется как замена для Microcal Origin - программа для несложной статистической обработки данных, построения всяческих графиков;
Grace6 (http://plasma-gate.weizmann.ac.il/Grace/) - программа для подготовки двумерных графиков по численным данным;
PAW (http://cern.ch/paw/) - интерактивная программа анализа и графического представления результатов. Может применяться для анализа большого и очень большого объёма данных;
ROOT (http://cern.ch/root/) - наследник PAW, интерактивная система обработки и визуализации очень больших объёмов научных данных;
GNU R (http://r-project.org/) - мощный язык статистических вычислений, используемый профессиональными статистиками;
GRETL (http://gretl.sourceforge.net/) - система эконометрического анализа;

Научные редакторы:
TeXLive - полноценный дистрибутив TeX;
TeXmacs (http://texmacs.org) - текстовый редактор для набора математических и прочих научных текстов, также позволяет включать в документ сессии Axiom, Maxima, Octave, SciLab и других систем компьютерной математики;
Kile (http://kile.sourceforge.net/) - интегрированная среда подготовки документов с помощью TeX;
Texmaker (http://www.xm1math.net/texmaker/) - интегрированная оболочка для LaTeX;

Также LiveMath III содержит среду Gnome 2.28, OpenOffice.org 3.1, Gnumeric. Для "больших" систем (ROOT, PAW, R, Octave) включена значительная часть имеющихся в репозиториях Ubuntu пакетов. Для многих изначально "консольных" систем включены GUI-обёртки, для некоторых по несколько, на выбор. К большинству программ есть документация. Возможна установка системы на жёсткий диск с помощью стандартного установщика Ubuntu.

UPD. Полный список установленных пакетов: http://iportnov.ru/files/LiveMath.packages.txt

К сожалению, у меня нет времени, чтобы тестировать все эти программы. То, что я протестировал - работает. Багрепорты принимаются в комментариях или на e-mail portnov at bk dot ru, но мгновенного исправления не обещаю.

LiveMath сделан с помощью Ubuntu Construction Kit (http://uck.sourceforge.net/), так что каждый, в принципе, может сделать себе нечто подобное. Вероятно, это окажется проще, чем качать моё изделие.

Взять можно здесь: http://portnov.homelinux.net/LiveMath%20III.iso (размер образа - 2Gb), может быть удобнее окажется торрент: http://iportnov.ru/files/LiveMath%20III.iso.torrent (честно говоря, не знаю, заработает ли). У меня сейчас нет хостинга, на котором я бы мог размещать большие ISO-образы. Так что учтите, что portnov.homelinux.net - это мой домашний сервер, обычно бывает включён примерно с 8:00 до 22:00 MSK, суперскоростей не обещаю. Если кому-то позарез нужно скачать в другое время - пишите, так уж и быть, оставлю включённым на ночь :)

суббота, марта 13, 2010

Ядро Linux за 10 минут (обзор)


Это конспект доклада для семинара, проведённого нашей LUG совместно с университетом.


У меня, натурально, было 10 минут, поэтому изложение — галопом по европам, многое упрощено, многое упущено.


Немного истории

Относительно подробную историю создания ядра Linux можно найти в известной книге Линуса Торвальдса «Just for fun». Нас из неё интересуют следующие факты:

  • Ядро создал в 1991 году студент университета Хельсинки Линус Торвальдс;

  • В качестве платформы он использовал ОС Minix, написанную его преподавателем Эндрю Таненбаумом, запущенную на персональном компьютере с процессором Intel 80386;

  • В качестве примера для подражания он использовал ОС семейства Unix, а в качестве путеводителя — сначала стандарт POSIX, а затем просто исходные коды программ из комплекта GNU (bash, gcc и пр).

Эти факты в значительной мере определили пути развития ядра в дальнейшем, их следствия заметны и в современном ядре.

В частности, известно, что Unix-системы в своё время разделились на два лагеря: потомки UNIX System V Release 4 (семейство SVR4) против потомков Berkley Software Distribution v4.2 (BSD4.2). Linux по большей части принадлежит к первому семейству, но заимствует некоторые существенные идеи из второго.

Ядро в цифрах

  • Около 30 тыс. файлов
  • Около 8 млн. строк кода (не считая комментариев)
  • Репозиторий занимает около 1 Гб
  • linux-2.6.33.tar.bz2: 63 Mb
  • patch-2.6.33.bz2: 10Mb, около 1.7 млн изменённых строк
  • Около 6000 человек, чей код есть в ядре

Об архитектуре ядра

Все (или почти все) процессоры, которыми когда-либо интересовались производители Unix-подобных ОС, имеют аппаратную поддержку разделения привелегий. Один код может всё (в т.ч. общаться напрямую с оборудованием), другой — почти ничего. Традиционно говорят о «режиме ядра» (kernel land) и «режиме пользователя» (user land). Различные архитектуры ядер ОС различаются прежде всего подходом к ответу на вопрос: какие части кода ОС должны выполняться в kernel land, а какие — в user land? Дело в том, что у подавляющего большинства процессоров переключение между двумя режимами занимает существенное время. Выделяют следующие подходы:

  • Традиционный: монолитное ядро. Весь код ядра компилируется в один большой бинарный файл. Всё ядро исполняется в режиме ядра;

  • Противоположный, новаторский: микроядро. В режиме ядра выполняются только самые необходимые части, всё остальное — в режиме пользователя;

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

  • И, конечно, всевозможные варианты гибридных архитектур.

Ядро Linux начиналось как монолитное (глядя на существовавшие тогда Unix-ы). Современное Linux-ядро модульное. По сравнению с микроядром монолитное (или модульное) ядро обеспечивает существенно бо́льшую производительность, но предъявляет существенно более жёсткие требования к качеству кода различных компонентов. Так, в системе с микроядром «рухнувший» драйвер ФС будет перезапущен без ущерба для работы системы; рухнувший драйвер ФС в монолитном ядре — это Kernel panic и останов системы.

Подсистемы ядра Linux

Существует довольно широко известная диаграмма, изображающая основные подсистемы ядра Linux и их взаимодействие. Вот она:

: linux-kernel-big.png

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

: linux-kernel-simple.png

Системные вызовы

Уровень системных вызовов — это наиболее близкая к прикладному программисту часть ядра Linux. Системные вызовы предоставляют интерфейс, используемый прикладными программами — это API ядра. Большинство системных вызовов Linux взяты из стандарта POSIX, однако есть и специфичные для Linux системные вызовы.

Здесь стоит отметить некоторую разницу в подходе к проектированию API ядра в Unix-системах с одной стороны и в Windows[NT] и других идеологических потомках VMS с другой. Дизайнеры Unix предпочитают предоставить десять системных вызовов с одним параметром вместо одного системного вызова с двадцатью параметрами. Классический пример — создание процесса. В Windows функция для создания процесса — CreateProcess() — принимает 10 аргументов, из которых 5 — структуры. В противоположность этому, Unix-системы предоставляют два системных вызова (fork() и exec()), первый — вообще без параметров, второй — с тремя параметрами.

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

Управление памятью

Ядро Linux использует в качестве минимальной единицы памяти страницу. Размер страницы может зависеть от оборудования; на x86 это 4Кб. Для хранения информации о странице физической памяти (её физический адрес, принадлежность, режим использования и пр) используется специальная структура page размером в 40 байт.

Ядро использует возможности современных процессоров для организации виртуальной памяти. Благодаря манипуляциям с каталогами страниц виртуальной памяти, каждый процесс получает адресное пространство размером в 4Гб (на 32х-разрядных архитектурах). Часть этого пространства доступна процессу только на чтение или исполнение: туда отображаются интерфейсы ядра.

Существенно, что процесс, работающий в пространстве пользователя, в большинстве случаев «не знает», где находятся его данные: в ОЗУ или в файле подкачки. Процесс может попросить у системы выделить ему память именно в ОЗУ, но система не обязана удовлетворять такую просьбу.

Управление процессами

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

В истории было известно два типа многозадачности:

Корпоративная многозадачность.

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

Вытесняющая многозадачность.

Ядро ОС выделяет каждому процессу определённый квант процессорного времени и «насильно» передаёт управление другому процессу по истечении этого кванта. Это создаёт накладные расходы на переключение режимов процессора и расчёт приоритетов, но повышает надёжность и производительность.

Переключение процессов в linux может производиться по наступлению двух событий: аппаратного прерывания или прерывания от таймера. Частота прерываний таймера устанавливается при компиляции ядра в диапазоне от 100Гц до 1000Гц. Аппаратные прерывания возникают чуть ли не чаще: достаточно двинуть мышку или нажать кнопку на клавиатуре, да и внутренние устройства компьютера генерируют прерывания. Начиная с версии 2.6.23, появилась возможность собрать ядро, не использующее переключение процессов по таймеру. Это позволяет снизить энергопотребление в режиме простоя компьютера.

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

Кроме многозадачности в режиме пользователя, ядро Linux использует многозадачность в режиме ядра: само ядро многопоточно.

Традиционные ядра Unix-систем имели следующую… ну если не проблему, то особенность: само ядро не было вытесняемым. Пример: процесс /usr/bin/cat хочет открыть файл /media/cdrom/file.txt и использует для этого системный вызов open(). Управление передаётся ядру. Ядро обнаруживает, что файл расположен на CD-диске и начинает инициализацию привода (раскручивание диска и пр). Это занимает существенное время. Всё это время управление не передаётся пользовательским процессам, т.к. планировщик не активен в то время, когда выполняется код ядра. Все пользовательские процессы ждут завершения этого вызова open().

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

Сетевая подсистема

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

Сетевая подсистема Linux обеспечивает следующую функциональность:

  • Абстракцию сокетов;

  • Стеки сетевых протоколов (TCP/IP, UDP/IP, IPX/SPX, AppleTalk и мн. др);

  • Маршрутизацию (routing);

  • Пакетный фильтр (модуль Netfilter);

  • Абстракцию сетевых интерфейсов.

В различных Unix-системах использовалось два различных прикладных интерфейса, обеспечивающих доступ к функциональности сетевой подсистемы: Transport Layer Interface (TLI) из SVR4 и sockets (сокеты) из BSD. Интерфейс TLI, с одной стороны, тесно завязан на подсистему STREAMS, отсутствующую в ядре Linux, а с другой — не совместим с интерфейсом сокетов. Поэтому в Linux используется интерфейс сокетов, взятый из семейства BSD.

Файловая система

Виртуальная файловая система (VFS)

С точки зрения приложений, в Unix-подобных ОС существует только одна файловая система. Она представляет собой дерево директорий, растущее из «корня». Приложениям, в большинстве случаев, не интересно, на каком носителе находятся данные файлов; они могут находиться на жёстком диске, оптическом диске, флеш-носителе или вообще на другом компьютере и другом континенте. Эта абстракция и реализующая её подсистема называется виртуальной файловой системой (VFS).

Стоит заметить, что VFS в ядре Linux реализована с учётом идей из ООП. Например, ядро рассматривает набор структур inode, каждая из которых содержит (среди прочего):

  • Данные из on-disk inode (права доступа, размер файла и др);

  • Указатель на структуру, описывающую драйвер ФС, к которой принадлежит данный inode;

  • Указатель на струкруру операций с inode, которая, в свою очередь, содержит указатели на функции для создания inode, изменения его атрибутов и т.д., реализованные в конкретном драйвере ФС.

Аналогично устроены структуры ядра, описывающие другие сущности ФС — суперблок, элемент каталога, файл.

Драйверы ФС

Драйверы ФС, как можно заметить из диаграммы, относятся к гораздо более высокому уровню, чем драйверы устройств. Это связано с тем, что драйверы ФС не общаются ни с какими устройствами. Драйвер файловой системы лишь реализует функции, предоставляемые им через интерфейс VFS. При этом данные пишутся и читаются в/из страницы памяти; какие из них и когда будут записаны на носитель — решает более низкий уровень. Тот факт, что драйверы ФС в Linux не общаются с оборудованием, позволил реализовать специальный драйвер FUSE, который делегирует функциональность драйвера ФС в модули, исполняемые в пространстве пользователя.

Страничный кэш

Эта подсистема ядра оперирует страницами виртуальной памяти, организованными в виде базисного дерева (radix tree). Когда происходит чтение данных с носителя, данные читаются в выделяемую в кэше страницу, и страница остаётся в кэше, а драйвер ФС читает из неё данные. Драйвер ФС пишет данные в страницы памяти, находящиеся в кэше. При этом эти страницы помечаются как «грязные» (dirty). Специальный поток ядра, pdflush, регулярно обходит кэш и формирует запросы на запись грязных страниц. Записанная на носитель грязная страница вновь помечается как чистая.

Уровень блочного ввода-вывода

Эта подсистема ядра оперирует очередями (queues), состоящими из структур bio. Каждая такая структура описывает одну операцию ввода-вывода (условно говоря, запрос вида «записать вот эти данные в блоки ##141-142 устройства /dev/hda1»). Для каждого процесса, осуществляющего ввод-вывод, формируется своя очередь. Из этого множества очередей создаётся одна очередь запросов к драйверу каждого устройства.

Планировщик ввода-вывода

Если выполнять запросы на дисковый ввод-вывод от приложений в том порядке, в котором они поступают, производительность системы в среднем будет очень низкой. Это связано с тем, что операция поиска нужного сектора на жёстком диске — очень медленная. Поэтому планировщик обрабатывает очереди запросов, выполняя две операции:

  • Сортировка: планировщик старается ставить подряд запросы, обращающиеся к находящимся близко секторам диска;

  • Объединение: если в результате сортировки рядом оказались несколько запросов, обращающихся к последовательно расположенным секторам, их нужно объединить в один запрос.

В современном ядре доступно несколько планировщиков: Anticipatory, Deadline, CFQ, noop. Существует версия ядра от Con Kolivas с ещё одним планировщиком — BFQ. Планировщики могут выбираться при компиляции ядра либо при его запуске.

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

Обработка прерываний

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

Тут существует определённая тонкость. Дело в том, что во время работы обработчика прерывания планировщик задач не активен. Это не удивительно: предполагается, что обработчик прерывания работает непосредственно с устройством, а устройство может требовать выполнения каких-то действий в жёстких временных рамках. Поэтому если обработчик прерывания будет работать долго, то все остальные процессы и потоки ядра будут ждать, а это обычно недопустимо.

В ядре Linux в результате любого аппаратного прерывания управление передаётся в функцию do_IRQ(). Эта функция использует отдельную таблицу зарегистрированных в ядре обработчиков прерываний, чтобы определить, куда передавать управление дальше.

Чтобы обеспечить минимальное время работы в контексте прерывания, в ядре Linux используется разделение обработчиков на верхние и нижние половины. Верхняя половина — это функция, которая регистрируется драйвером устройства в качестве обработчика определённого прерывания. Она выполняет только ту работу, которая безусловно должна быть выполнена немедленно. Затем она регистрирует другую функцию (свою нижнюю половину) и возвращает управление. Планировщик задач передаст управление зарегистрированной верхней половине, как только это будет возможно. При этом в большинстве случаев управление передаётся нижней половине сразу после завершения работы верхней половины. Но при этом нижняя половина работает как обычный поток ядра, и может быть прервана в любой момент, а потому она имеет право исполняться сколь угодно долго.

В качестве примера можно рассмотреть обработчик прерывания от сетевой карты, сообщающего, что принят ethernet-пакет. Этот обработчик обязан сделать две вещи:

  • Взять пакет из буфера сетевой карты и сигнализировать сетевой карте, что пакет получен операционной системой. Это нужно сделать немедленно по получении прерывания, через милисекунду в буфере будут уже совсем другие данные;

  • Поместить этот пакет в какие-либо структуры ядра, выяснить, к какому протоколу он относится, передать его в соответствующие функции обработки. Это нужно сделать как можно быстрее, чтобы обеспечить максимальную производительность сетевой подсистемы, но не обязательно немедленно.

Соответственно, первое выполняет верхняя половина обработчика, а второе — нижняя.

Драйвера устройств

Большинство драйверов устройств обычно компилируются в виде модулей ядра. Драйвер устройства получает запросы с двух сторон:

  • От устройства — через зарегистрированные драйвером обработчики прерываний;

  • От различных частей ядра — через API, который определяется конкретной подсистемой ядра и самим драйвером.

воскресенье, января 03, 2010

Текущие проекты

Давно я что-то сюда не писал. Замотался совсем. В частности, несколько неожиданно для себя стал техническим писателем :)

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

Framework

Это фреймворк (не очень высокого уровня, на настоящий момент) для создания web-приложений на Haskell. Страница проекта тут, haddock-документация тут. Проект в значительной мере исследовательский: насколько сложно/просто писать веб-приложения на Haskell? А фреймворки? Какие новые идеи способен привнести Haskell в эту область? Кроме того, изначально я задумывал фреймворк для разработки приложений высокой нагруженности (так что само собой предполагаются всякие кэширования, работа со многими СУБД и мн.др.). Во фреймворке в настоящий момент много чего не хватает (начиная с названия) — нет полноценной ORM, нет генерации произвольных диалектов SQL… Вероятно, как раз в этих областях что-нибудь интересное получится в результате. Кое что [на мой взгляд] оригинальное в фреймворке уже есть. Т.к. Haskell — компилируемый язык, то всё приложение — это один бинарник. Включая шаблоны. Шаблоны пишутся в синтаксисе, похожем на Django-вский (вообще, я многие идеи старался взять из django), при сборке приложения по ним генерируется haskell-исходник и компилируется вместе с приложением. Достоинства и недостатки, собственно, очевидны: нет затрат времени на парсинг шаблонов на каждый запрос (но и затрат сложности на кэширование шаблонов тоже нет), генерация html по шаблонам быстрее, но при изменении шаблонов надо пересобирать приложение (но если речь идёт о большой нагрузке, шаблоны будут меняться редко).

MyPaint

Как несложно догадаться из названия, MyPaint (http://mypaint.intilinux.com) — это программа для рисования (дословно — что-то вроде "моя живопись"; исторически, это название — ссылка на программу paint.exe от microsoft). Программ для рисования сейчас довольно много, в том числе и свободных, и под Linux (конечно, в первую очередь на ум приходит Gimp). Особенность MyPaint — это программа в первую очередь именно для рисования, а не для обработки готовых изображений (собственно, MyPaint даже не умеет таких вещей, как "кроп" или "уровни"; за такими функциями добро пожаловать в тот же Gimp). На самом деле, ближайшие конкуренты MyPaint — это Corel Painter и ArtRage (NB: это не означает, что они идут ноздря-в-ноздрю, просто это программы одного назначения).

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

Коротко изменения — i18n и перевод на русский (сейчас уже в основной ветке, вместе с переводами на французский, норвежский, шведский, упрощённый китайский и др.); палитра; что-то наподобие масок; диалог слоёв; группировка кистей; поддержка наклона пера. Подробнее на вики mypaint, там же рядом бурное обсуждение интерфейса.

Надеюсь в ближайшее время сделать отдельную статью про MyPaint. А пока, «с первого и по тринадцатое», собираюсь поплотнее заняться разработкой с целью сделать мои нововведения пригодными для вливания в основную ветку — релиз планируется сразу после этого мержа.

Todos

Ещё один проект без нормального названия :) Это простецкий TODO-менеджер на Haskell. Собственно, сами TODO пишутся в любом текстовом редакторе в plain-text файлике (желательно, с названием TODO) в простецком формате:

[spaces]status [TAGS] title (depends) description

где [spaces] — отступ пробелами, status — состояние задачи, [TAGS] — список тегов в квадратных скобках через пробел, title — заголовок или описание, (depends) — список зависимостей (заголовков других записей) в скобках через запятую, description — описание. Все поля кроме статуса и заголовка необязательны. Отступами определяется подчинённость записей, благодаря зависимостям (которые в скобках) структура может быть не только деревом, но произвольным графом (даже циклическим). Собираюсь приделать поддержку дат (чтобы, например, можно было отобрать дела, запланированные на завтра).

Сама программа только отбирает записи из файла по условиям, заданным в командной строке (см. вывод todos --help). Фильтровать можно по любому из полей. Есть «сложные» запросы, вида «задачи с тегом BUG и статусом отличным от FIXED», правда парсер таких запросов работает пока не идеально.

Смотреть/брать код здесь: http://gitorious.org/todos/. Компилируется GHC 6.10.4. Из зависимостей — пакет text-regex-pcre.