Как OCaml представляет ленивые значения во время выполнения? - PullRequest
7 голосов
/ 25 июня 2019

Эта глава в реальном мире OCaml описывает структуру памяти времени выполнения для различных типов данных.Однако обсуждение ленивых значений не ведется.

  • Как реализовано lazy_t, т. Е. Что представляет его представление во время выполнения и какие ключевые операции являются встроенными компиляторами?Ссылки на исходный код приветствуются.Я посмотрел на модуль CamlinternalLazy , но реальное представление, кажется, трудно расшифровать только на основе вызовов функций из модуля Obj.
  • Может ли кто-нибудь предоставить сводку сделанных измененийв представление / операции, чтобы сделать его потокобезопасным для многоядерного проекта OCaml?Этот коммит , кажется, является тем, с реализацией, но он кажется немного непрозрачным для меня как постороннего.

Примечание: Этот вопрос о Компилятор OCaml / время выполнения.Я понимаю, что нет стандартной спецификации для того, как ленивые значения должны быть реализованы компилятором / средой выполнения OCaml.

1 Ответ

7 голосов
/ 25 июня 2019

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

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

# Obj.repr (lazy 42) == Obj.repr 42;;
- : bool = true

# Obj.tag (Obj.repr sin) = (Obj.tag (Obj.repr (lazy sin)));;
- : bool = true

# Obj.closure_tag = (Obj.tag (Obj.repr (lazy sin)));;
- : bool = true

То же самое верно для типов, которые обычно имеют представление в штучной упаковке, например строки,

let s = "hello" in
Obj.repr s == Obj.repr (lazy s);;
- : bool = true

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

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

type 'a value = Deferred of (unit -> 'a) | Ready of 'a 
type 'a lazy_t = {
  mutable lazy : 'a value;
}

и оператор lazy захватывает вложенное выражение, т. Е. На синтаксическом уровнеязык, он переводит что-то вроде этого:

lazy x => {lazy = Deferred (fun () -> x)

Вот некоторые взаимодействия с OCaml, которые демонстрируют представление:

let x = lazy (2+2) in
Obj.lazy_tag = Obj.tag (Obj.repr x);;
- : bool = true

let x = lazy (2+2) in
let _ = Lazy.force x in
Obj.forward_tag = Obj.tag (Obj.repr x);;
- : bool = true

Как мы видим, вычисления хранятся в виде thunk (ииспользует 4 слова)

let x = lazy (2+2) in
Obj.reachable_words (Obj.repr x);;
  - : int = 4

, в то время как после принудительного вычисления оно будет сохранено как переадресованный (упакованный) int,

let x = lazy (2+2) in
let _ = Lazy.force x in
Obj.reachable_words (Obj.repr x);;
- : int = 2

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

let x = lazy (raise Not_found) in 
Obj.lazy_tag = Obj.tag (Obj.repr x);;
- : bool = true

let x = lazy (raise Not_found) in 
try Lazy.force x with Not_found -> 
Obj.lazy_tag = Obj.tag (Obj.repr x)

С точки зрения реализации, вычисление, которое вызывает исключение, заменяется функцией, которая вызывает это исключение.Таким образом, все еще происходит некоторое запоминание, другими словами, если у вас было lazy (x (); y (); z ()) и y () вызывает исключение E, тогда полезная нагрузка ленивого значения будет заменена функцией fun () -> raise E, то есть она никогда не будетповторите x (), и он никогда не достигнет z ().

Lazy-значения в Multicore

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

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

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

Прежде чем мы углубимся в реализацию, есть еще одна вещь, которая должна быть объяснена относительно ленивых значений в OCaml.Когда ленивое значение форсируется, оно не сразу обновляется до результата вычисления, поскольку само вычисление может быть рекурсивным и ссылаться на ленивое значение.Вот почему на первом шаге перед вызовом вычисления, присоединенного к ленивому значению, полезная нагрузка ленивой функции заменяется функцией, которая вызывает исключение Lazy.Undefined, так что неправильно сформированные рекурсивные выражения по-прежнему хорошо завершаются.

Эта уловка была перехвачена и повторно использована Группой Multicore, чтобы сделать ленивые значения безопасными в присутствии нескольких потоков, пытающихся форсировать его одновременно.Когда ленивое значение форсируется, они заменяют его полезную нагрузку функцией, называемой bomb, которая проверяет, ссылаются ли на ленивое значение снова (либо потому, что вычисление повторяется, либо потому, что оно используется другим потоком) во время оценки, и еслиссылка находится в том же домене, после чего запускается исключение Undefined, указывающее, что это не правильно сформированное ленивое значение, или если домен отличается, то возникает исключение RacyLazy, которое указывает на наличие несериализованногодоступ к одному и тому же ленивому значению из разных доменов.

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

Ссылки на реализацию

Это

...