/
Поиск
RU
ENRU

Ресурсы и линейность

Некоторые значения обозначают что-то за пределами памяти вашей программы. Файловый дескриптор — небольшое целое число, которое операционная система выдаёт на открытый файл или сокет; запись о нём хранится в таблице ОС, пока вы его не закроете, и процесс, который открывает файлы и не закрывает их, рано или поздно упирается в лимит. Блокировку нужно отпустить, иначе все потоки, которые её ждут, зависнут. Транзакцию базы данных нужно зафиксировать или откатить. За каждым таким значением стоит обязательство. В C оно живёт в комментарии. В C++ и Rust его незаметно выполняет деструктор — функция, которую компилятор сам вызывает, когда значение выходит из области видимости. kola не делает ни того, ни другого. Такие значения объявляются линейными ресурсами, и компилятор требует, чтобы каждый ресурс был израсходован ровно один раз на каждом пути выполнения. Забыть что-то закрыть — ошибка компиляции. Неявных деструкторов нет: очистка — обычный вызов функции, который видно в исходном тексте.

Чем ресурс отличается от структуры

Синтаксически разница в одном слове: resource struct вместо struct. Меняются правила обращения со значением:

struct / enum (данные)

resource struct (ресурс)

Присваивание, передача

Копируется: оба имени остаются годными

Перемещается: владение уходит дальше, старое имя мертво

Конец жизни

Выходит из области видимости

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

Для чего

Простая информация: точки, размеры, вердикты

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

Для данных let b = a; создаёт вторую копию, и обе остаются годными. Для ресурса та же строка передаёт владение: теперь значение называется b, и любое последующее обращение к a — ошибка компиляции. Копии быть не может: два владельца одного файла закрыли бы его дважды. Такое же перемещение происходит в любой позиции «по значению», не только в let: в аргументе функции, в поле литерала структуры, в Some(v), в возвращаемом значении, в сообщении, отправленном в канал.

Первый ресурс

Сквозной пример — журнал упреждающей записи (write-ahead log): файл, в который база данных дописывает записи до того, как применить их, чтобы восстановиться после сбоя. Наш журнал нужно запечатать, когда работа с ним закончена. Наведите курсор на выделенные места:

use std::log;

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} {
        Wal { entries: 0 }
    }

    pub fn append(self: &mut Wal) !{} {
        self.entries = self.entries + 1;
    }

    pub fn seal(self: Wal) !{log} {
        log::info(f"sealed after {self.entries} entries");
        let Wal { entries: _ } = self;
    }
}

fn main() -> u8 !{log} {
    let mut wal = Wal::open();
    wal.append();
    wal.append();
    log::info(f"entries so far: {wal.entries}");
    wal.append();
    wal.seal();
    0
}

seal не принимает никакой капабилити: дескриптор сам несёт свои полномочия. Для записи в журнал тоже ничего не нужно, потому что log — эффект, а не ресурс (см. Эффекты и капабилити).

Удалите wal.seal();, и компилятор укажет на объявление:

error[card §2]: resource `wal` is not consumed on this path
  --> wal.kl:21:5
    |
 21 |     let mut wal = Wal::open();
    |     ^^^
    = help: no implicit destructors: move it on, return it, destructure it, or pass it to a consuming fn

Деструктуризация

В let Wal { entries: _ } = self; слева стоит образец в форме Wal; entries: _ отбрасывает это поле, а entries: n сохранило бы его. Как только образец сопоставлен, ресурса больше нет. Это тело деструктора, только написанное там, где его видно.

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

resource struct Txn { id: u64, writes: u32 }

impl Txn {
    pub fn begin(id: u64) -> Txn !{} { Txn { id: id, writes: 0 } }
    pub fn record(self: &mut Txn) !{} { self.writes = self.writes +% 1; }
    pub fn commit(self: Txn) -> u32 !{} {
        let Txn { id: _, writes: w } = self;
        w
    }
}

test destructure_binds_a_field {
    let mut t = Txn::begin(42);
    t.record();
    t.record();
    t.record();
    let n = t.commit();           // расходует t, возвращает число записей
    assert n == 3;
}

Пропустите поле, и образец будет отвергнут:

error[card §2]: struct pattern misses field `id`
  --> txn.kl:6:9
   |
 6 |         let Txn { writes: w } = self;
   |         ^^^
   = help: destructuring consumes the whole value; name every field (use `_`)

Израсходовать ресурс можно четырьмя способами: передать в расходующую функцию (wal.seal()), вернуть, переместить дальше (let archived = wal;, в структуру, в канал, в другую функцию) или деструктурировать. Одно из этого должно случиться ровно один раз на каждом пути через функцию, включая ранние возвраты и каждую ветку match. Компилятор отвергает и забытый случай, и двойной.

? — это ранний возврат

«Каждый путь» включает и те пути, которые вы не выписывали. Оператор ? (см. Контракты, трапы и тесты) — скрытый return Err(...), и ресурс, живой в точке ?, потерялся бы на ветке ошибки. Чекер об этом сообщает и показывает, где ресурс объявлен:

error[card §2]: `?` returns early on Err while resource `w` is live — the Err path would leak it
  --> ingest.kl:10:13
    |
 10 |     let v = step(b)?;
    |             ^^^^^^^^
    = help: consume `w` before the `?`, or handle the Result with an explicit `match`
    = note: `w` was declared here (ingest.kl:9:5)

Либо закончите с ресурсом до вызова, который может не удаться, либо выпишите match явно, и тогда придётся сказать, что происходит с ресурсом в каждой ветке:

use std::log;

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} { Wal { entries: 0 } }
    pub fn append(self: &mut Wal) !{} { self.entries = self.entries + 1; }
    pub fn seal(self: Wal) !{log} {
        log::info(f"sealed after {self.entries} entries");
        let Wal { entries: _ } = self;
    }
    pub fn discard(self: Wal) !{} { let Wal { entries: _ } = self; }
}

enum ParseErr { Short }

fn parse_len(b: &[u8]) -> Result[u32, ParseErr] !{} {
    if b.len == 0 { return Err(ParseErr::Short); }
    Ok(widen[u32](b[0]))
}

fn ingest(b: &[u8]) -> Result[u32, ParseErr] !{log} {
    let n = parse_len(b)?;       // живых ресурсов пока нет — можно
    let mut w = Wal::open();
    w.append();
    match parse_len(b) {         // `?` здесь отвергли бы: `w` жив
        Ok(v) => { w.seal(); Ok(n +% v) }
        Err(e) => { w.discard(); Err(e) }
    }
}

test question_mark_and_linearity {
    let good = ingest(&b"\x05");
    assert good == Ok(10u32);
    let bad = ingest(&b"");
    assert bad == Err(ParseErr::Short);
}

lend: представление, которое можно сохранить

Для обычного доступа ничего особенного не нужно: чтение поля (wal.entries) или вызов метода (wal.append()) заимствует ресурс на время выражения или вызова. lend нужен, когда требуется ссылка в регион &r Wal: обычно чтобы сложить представления нескольких ресурсов в структуру данных в регионе или передать одно из них функции, которая хранит ссылки. let v: &r Wal = lend wal in r; замораживает wal до закрытия региона. До тех пор wal нельзя ни изменить, ни израсходовать:

error[card §4]: `a` is frozen by a `lend` until its region closes
  --> lend.kl:11:9
    |
 11 |         a.append();
    |         ^

Представление доступно только для чтения; lend mut не существует. Когда регион закрывается, заморозка снимается, и владельца снова можно менять и расходовать. Одалживать один и тот же ресурс в один и тот же регион дважды можно. lend никогда не считается расходованием, так что к закрытию региона обязательство никуда не девается.

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

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} { Wal { entries: 0 } }
    pub fn append(self: &mut Wal) !{} { self.entries = self.entries + 1; }
    pub fn discard(self: Wal) !{} { let Wal { entries: _ } = self; }
}

test lend_into_a_structure {
    let mut a = Wal::open();
    a.append();
    let mut b = Wal::open();
    b.append();
    b.append();

    region r {
        let views: &r mut Vec[&r Wal] = alloc in r mut Vec::new();
        views.push(lend a in r);     // с этого места a и b заморожены
        views.push(lend b in r);

        let mut total: u32 = 0;
        for i in 0..views.len {
            total = total +% views[i].entries;
        }
        assert total == 3;
    }
    a.discard();                     // регион закрыт: a снова доступен
    b.discard();
}

Затенение живого ресурса

Переопределять имя вторым let для данных можно, как в Rust. Живой ресурс так спрятать нельзя: одна невинная на вид строка привела бы к утечке.

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} { Wal { entries: 0 } }
    pub fn discard(self: Wal) !{} { let Wal { entries: _ } = self; }
}

test shadowing_a_live_resource {
    let wal = Wal::open();
    let wal = Wal::open();   // первый Wal всё ещё жив
    wal.discard();
}

Компилятор сообщает resource `wal` is not consumed on this path на первом let. Сначала израсходуйте первое значение, потом используйте имя заново.

Необязательные ресурсы

Ресурс часто лежит в слоте, который иногда пуст: рабочий поток, который ещё не запущен, соединение, которое то ли открыто, то ли нет. Слот — это Option, и линейность следит за тем, что в нём лежит. Option со значением None на выходе ничего не должен, а присваивание в него ничего не теряет, так что заполнить пустой слот — обычный код. Some(ресурс) несёт обязательство, и match снимает его в обеих ветках. Перезаписать слот, в котором действительно лежит ресурс, по-прежнему нельзя, как нельзя и цикл, который на каждом проходе заполняет слот, не опустошив его: он терял бы по ресурсу за итерацию.

Чтобы вынуть значение из слота, в который можно писать (&mut Option[T], поле структуры за &mut, элемент &mut Vec), есть take(): он возвращает значение и оставляет на его месте None.

resource struct Wal { entries: u32 }

impl Wal {
    pub fn open() -> Wal !{} { Wal { entries: 0 } }
    pub fn discard(self: Wal) !{} { let Wal { entries: _ } = self; }
}

// Опустошить слот, если в нём что-то есть, и оставить None.
fn retire(slot: &mut Option[Wal]) -> bool !{} {
    match slot.take() {
        Some(w) => { w.discard(); true }
        None => false,
    }
}

test an_empty_slot_owes_nothing {
    let mut slot: Option[Wal] = None;     // пуст, ничего не должен
    slot = Some(Wal::open());             // теперь должен одно расходование
    let retired = retire(&mut slot);
    assert retired;
    match slot {                          // чекер не знает, что слот уже None,
        Some(w) => { w.discard(); }       // поэтому на выходе всё равно match
        None => {}
    }
}

Инварианты

Инвариант — условие, которое выполняется для каждого значения типа, пока это значение существует: счётчик не превышает 100, голова кольцевого буфера меньше его размера. Без поддержки языка такие условия живут в комментариях, и каждая функция либо верит им, либо проверяет заново. resource struct объявляет их последним элементом своего тела:

resource struct Counter { n: u32, inv n <= 100 }

impl Counter {
    pub fn bump(self: &mut Counter) !{} {
        self.n = self.n + 1;
    }
    pub fn done(self: Counter) -> u32 !{} {
        let Counter { n } = self;
        n
    }
}

test invariant_holds {
    let mut c = Counter { n: 0 };
    c.bump();
    c.bump();
    let total = c.done();    // сначала привязать: assert не может расходовать и менять
    assert total == 2;
}

Попытка создать Counter { n: 200 } вызывает трап прямо в месте создания с сообщением inv violated on `Counter`. Поэтому любая функция, получившая Counter, может полагаться на n <= 100 без проверок: другого Counter существовать не может. Инварианты подчиняются тем же правилам, что и прочие контракты: доказываются при компиляции, где это возможно, и проверяются во время выполнения в остальных случаях.

Ресурсы и domain

Трап — реакция kola на нарушенное допущение, например переполнение, выход индекса за границы или невыполненный контракт: выполнение останавливается в этой точке, без раскрутки стека. Обычно трап завершает весь процесс. domain ограничивает его одним блоком, domain d { work(); } recover(t: Trap) { ... }, чтобы сервер мог потерять запрос, а не самого себя. Трапам посвящена глава Контракты, трапы и тесты; здесь они появляются потому, что домен взаимодействует с линейностью.

Трап покидает блок посередине. У ресурса, который был жив в этот момент, на таком пути не было бы расходования, и компилятор уже не мог бы обещать «ровно один раз». Поэтому линейное значение нельзя ни объявить, ни использовать в теле домена или в его ветке recover. Маркеры полномочий (о них ниже) — исключение: если такой потерять, ничего не пропадёт. Если же в момент трапа ресурс ещё жив внутри вызванной функции, трап фатален, и никакой домен его не поймает.

error[card §3]: `w`: a linear resource may not live inside a `domain` — a trap would strand it
  --> worker.kl:9:9
   |
 9 |         let w = Wal::open();
   |         ^^^
   = help: domains compute over data; move this resource outside the domain, or consume it before entering

Работает такая форма: ресурс остаётся снаружи, а домен считает над простыми данными.

use std::log;

fn checked_div(a: u32, b: u32) -> u32 !{log} {
    let mut out: u32 = 0;
    domain d {
        out = a / b;             // трап при b == 0
    } recover(t: Trap) {
        let k = t.kind;          // Bounds, Arith, Req, Ens, Inv, Assert, ...
        let site = t.site;       // "module:line"
        log::warn(f"recovered {k} at {site}");
        out = 0;
    }
    out
}

test domain_bounds_the_trap {
    assert checked_div(10, 2) == 5;
    assert checked_div(10, 0) == 0;    // трап, восстановление, работа продолжается
}

Какие встроенные значения нужно расходовать

Линейность нужна не только типам, которые объявляете вы. На ней построена вся система капабилити (см. Эффекты и капабилити) и каждый дескриптор ОС, который выдаёт стандартная библиотека. Обязательства у них разные, и разница следует одному правилу: владеет ли значение чем-нибудь.

  • Маркеры полномочий можно бросить. Clock, Rng, Fs, Dir, DirRo, Dial, Listen, Stdout, Stdin, Args, Env, Tty, Ping, Proc, Mmio и его окна, Cpu, Dev, Window и сам Sys. Ни количества, которое нужно сверить, ни того, что нужно освободить, у них нет, поэтому бросить такой маркер ничего не стоит, и среда выполнения сама его заберёт. Маркер всё равно перемещается, а не копируется; чтобы дать рабочему потоку собственный, его ослабляют (clock.split(), dir.ro()).

  • Mem нужно вернуть. Это единственная измеряемая величина. sys.mem.split(n) отрезает бюджет памяти, а sys.mem.absorb(sub) возвращает его; если бросить его в промежутке, бюджет пропадёт до конца работы программы. Забудьте absorb, и получите знакомое resource `small` is not consumed on this path ещё при компиляции.

  • Линейные дескрипторы нужно закрыть. За ними стоит настоящий объект ОС или ключевой материал, и брошенный дескриптор — это утечка. Чаще всего встречаются такие: File, Tmp, Sealed, FsNode (файлы); Listener, Conn, UdpSock, Poller (сеть); Thread, Tx, Rx (потоки и каналы); Child, ChildIn, ChildOut (процессы); Device (узел устройства); Secret (брошенный, он оставил бы ключевой материал нестёртым); RawMode (брошенный, он оставил бы терминал в сыром режиме). Дескрипторы GUI и пакетных сокетов подчиняются тому же правилу.

Капабилити строга не потому, что могущественна, а потому, что чем-то владеет. Clock даёт широкие полномочия, и бросить его ничего не стоит; один File даёт узкие полномочия, и закрыть его обязательно. По той же причине имена встроенных линейных дескрипторов зарезервированы: struct Thread { ... } или struct Conn { ... } компилятор отвергнет, потому что spawn выдаёт Thread, а имени типа вы при этом не пишете, и двойник с тем же именем мог бы вывести живой дескриптор из-под линейности. Единственное исключение из правила «расходуйте всё сами» — корневой набор: всё, что осталось в sys, когда main возвращается (или в sim, когда заканчивается тест), забирает среда выполнения.

Нормативное описание — SPEC-CARD §2 и §7 (kola help spec-card).