In diesem Post geht es endlich mal wieder um
OCaml, eine großartige funktionale Sprache, die
es schon seit 1996 gibt. (Wenn man den Vorgänger Caml mitzählt sogar
schon seit 1985.)
OCaml hat wie viele andere funktionale Sprachen seinen Ursprung in der
Forschung am INRIA in Frankreich, ist aber seit ca. 20 Jahren
zunehmend auch in industriellen Projekten im Einsatz, zum Beispiel bei
Facebook, Jane
Street und
Bloomberg.
Zum Erfolg von OCaml haben allem vor das elegante Modulsystem, die
ergonomische Syntax, der schnelle Byte-Code- und der effiziente
Native-Code-Compiler beigetragen. Ein Manko plagte aber die
OCaml-Programmierung seit den Anfangstagen: OCaml unterstützte bis
vor kurzem keine Multicore-Programmierung, zumindest nicht direkt.
Mit dem Release von OCaml 5.0.0 im
Dezember 2022 ist das Problem allerdings ausgeräumt:
Multicore-Programmierung sowie Nebenläufigkeit werden unterstützt.
Das Multicore-OCaml-Team um
KC Sivaramakrishnan hat sich viel Zeit
gelassen, um wirklich alles richtig zu machen.
„Multicore OCaml“ hat eine ganze Reihe von Facetten, heute geht es
speziell um die Nutzung von Betriebssystem-Threads. In späteren Posts
werden wir uns auch noch die Unterstützung von Nebenläufigkeit mit
„effect handlers“ anschauen sowie die effiziente parallele
Programmierung mit „Reagents“.
Was ist eigentlich ein Thread?
Um die Multicore-Unterstützung in OCaml einordnen zu können, klären
wir zunächst ein paar Begriffe:
Programmiersprachen, die Parallelismus oder Nebenläufigkeit
unterstützen, bieten häufig an, Code in „Threads“ auszuführen, wobei
mehrere Threads „gleichzeitig“ laufen können. Allerdings verstehen
unterschiedliche Sprachen beziehungsweise Laufzeitumgebungen darunter
sehr unterschiedliche Dinge:
-
„Betriebssystem-Threads“, die einen Thread in der
Programmiersprache auf einen Thread des Betriebssystems abbilden,
das für diesen dann das Scheduling insbesondere auf
Multicore-Systemen erledigt.
-
„Green Threads“, von
denen mehrere innerhalb eines Betriebssystem-Threads laufen können,
und deren Scheduling von der Laufzeitumgebung der Programmiersprache
erledigt wird.
Warum braucht man Green Threads?
Betriebssystem-Threads sind oft vergleichsweise teuer, was den
Platzverbrauch und den Zeitaufwand beim Start betrifft. (Weshalb es
dann zum Beispiel in Java „Thread Pools“ gibt, um die teuer erzeugten
Threads zu rezyklieren.) „Green Threads“ kommen in vielen
Programmiersprachen mit deutlich geringerem Overhead aus, insbesondere
in funktionalen Sprachen wie Erlang, Scheme oder Haskell.
Traditionell waren diese beiden Modelle eine
Entweder-Oder-Entscheidung: Programmiersprachen-Implementierungen mit
Green Threads haben traditionell beim Start eine feste Menge
Betriebssystem-Threads gestartet und auf denen dann das Scheduling der
Green Threads erledigt. Damit wurde aber der Scheduling-Prozess als
ganzer oft komplex und intransparent und nicht für alle Anwendungen
passend.
OCaml geht einen anderen Weg und gibt Programmierys direkten,
transparenten Zugriff auf die Betriebssystem-Threads. Das OCaml-Team
hat dabei besonders großen Wert darauf gelegt, dass alter Code ohne
nennenswerten Laufzeitverlust auch auf Multicore-OCaml läuft.
Multicore OCaml kommt außerdem mit einem „Green Thread Construction
Kit“: Man kann sich „Green Threads“ selber bauen, gegebenenfalls
maßgeschneidert für einen bestimmten Anwendungszweck. Darüber mehr,
wie gesagt, in einem zukünftigen Blog-Post.
In diesem Post geht es also um Betriebssystem-Threads in Multicore
OCaml. Rudimentäre OCaml-Kenntnisse setzen wir voraus.
Domains = Betriebssystem-Threads
Um Begriffskonfusion zu vermeiden, heißt die OCaml-Schnittstelle zu
Betriebssystem-Threads
„Domains“. Eine Domain ist eine
Berechnung, die in einem Betriebsystem-Thread abläuft und ein Ergebnis
produziert. DasDomain-Modul definiert entsprechend einen Typ für
Domains:
Ein OCaml-Modul kann also unter dem Damen Domain.t auf diesen Typ zugreifen.
Der Typparameter 'a ist der Typ des Ergebnisses.
Die beiden wesentlichen Funktionen zu Domains erlauben, eine Domain
zu starten und auf deren Beendigung zu warten:
val spawn : (unit -> 'a) -> 'a t
val join : 'a t -> 'a
Der Code in einer Domain kann mit anderen Domains über
Standard-Mechanismen der parallelen Programmierung kommunizieren -
über geteilten Zustand sowie
Mutexe und
Semaphoren und
Condition-Variablen, um den
Zugriff darauf zu koordinieren.
Diese Low-Level-Mechanismen sind für die tägliche Programmierung
allerdings ziemlich umständlich und fehleranfällig. Darum gibt es
eine praktische Library namens
Domainslib, die auf
der primitiven Domain-Funktionalität aufbaut. Sie bietet:
Kanäle
Für unser Code-Beispiel benutzen wir
Channels.
Ein Channel kann für die Übertragung von Nachrichten zwischen
zwei Domains benutzt werden. Der dazugehörige Typ ist:
Außerdem gibt es Funktionen zum Senden und Empfangen von Nachrichten:
val send : 'a t -> 'a -> unit
val recv : 'a t -> 'a
Nun ist jeder Channel mit einem Puffer versehen, in dem send Nachrichten
zunächst speichert, damit recv sie danach abholen kann.
Diesen Puffer gibt es in zwei Varianten, je nachdem, welche Funktion
zur Konstruktion verwendet wird:
val make_bounded : int -> 'a t
Diese Funktion macht einen Channel mit einem Puffer fester Größe.
Läuft er voll, blockiert send so lange, bis wieder Platz ist. Es
ist möglich, einen synchronen Channel zu machen – mit Puffergröße 0.
Dieser blockiert bei send immer, bis ein recv erfolgt,
beziehungsweise umgekehrt.
val make_unbounded : unit -> 'a t
Diese Funktion macht einen Puffer unbeschränkter Größe – send kann
hier gar nicht blockieren.
Von send und receive gibt es auch Varianten, die „pollen“, also
nicht blockieren können:
val send_poll : 'a t -> 'a -> bool
val recv_poll : 'a t -> 'a option
send_poll liefert true, wenn das Senden geklappt hat, und sonst
false. Bei recv_poll kommt Some <message> zurück, wenn eine
Nachricht wartete, sonst None.
Dinierende Philosophen
Um die Funktionalität von Multicore OCaml zu demonstrieren, nehmen wir
uns das
Philosophenproblem
vor – ein Klassiker der nebenläufigen Programmierung, ursprünglich
formuliert von Edsger W. Dijkstra.
Wikipedia beschreibt es so:
„Fünf Philosophen, nummeriert von 0 bis 4, leben in einem Haus, in dem
der Tisch für sie gedeckt ist, wobei jeder Philosoph seinen eigenen
Platz am Tisch hat. Ihr einziges Problem – neben dem der Philosophie –
ist, dass es sich bei dem servierten Gericht um eine sehr schwierige
Sorte Spaghetti handelt, die mit zwei Gabeln gegessen werden
muss. Zwischen den Tellern befindet sich jeweils eine Gabel, so dass
dies für einen einzelnen Philosophen kein Problem
darstellt. Allerdings können zwei Nachbarn nicht gleichzeitig essen.“
Wir realisieren die Lösung von Chandy und
Misra,
die folgendermaßen funktioniert:
- Die Gabeln können die Zustände „sauber“ und „schmutzig“ annehmen.
Am Anfang sind alle Gabeln schmutzig.
- Wenn einer der Philosophen essen will, müssen sie eine Anfrage an
den entsprechenden Nachbarn schicken.
- Wenn ein Philosoph mit einer Gabel eine Anfrage bekommt, beantwortet
er diese, sobald die Gabel schmutzig ist – dann macht er sie
zunächst sauber und gibt sie dann dem Anfragenden.
- Wenn ein Philosoph zwei saubere Gabeln hat, isst er und macht beide
Gabeln so schmutzig.
Wir erledigen erstmal die Domänenmodellierung. Bei den Gabeln wird
zwischen linker und rechter Gabel unterschieden:
type which_fork = Left | Right
Wir modellieren außerdem den „Zustand“ jeder Hand eines Philosophen
entsprechend dem Paper von Chandy/Misra:
type hand = No_fork | Requested | Dirty | Clean
Die Hand kann leer sein (No_fork), der Philosoph könnte den
Nachbar-Philosophen eine Anfrage auf die entsprechende Gabel geschickt
haben (Requested) und in der Hand könnte eine schmutzige oder eine
saubere Gabel liegen (Dirty beziehungsweise Clean).
Wir nummerieren die Philosophen durch und statten sie mit einem Kanal
aus, über den sie Gabeln oder Anfragen auf Gabeln bekommen können.
Wir nehmen außerdem eine Nachricht auf, die den Philosophen anweist,
seine Domain zu beenden:
type philosopher = { number: int; channel: message Domainslib.Chan.t }
and message =
| Heres_fork of which_fork
| Want_fork of philosopher * which_fork
| Die
Zur Bedeutung der Nachrichten:
- Mit der
Heres_fork-Nachricht schickt ein Philosoph A einem
Philosophen B die Gabel, und zwar mit den Links-/Rechts-Seiten von
Philosoph B.
- Mit der
Want_fork-Nachricht schickt Philosoph A einem Philosophen
B, wenn er eine Gabel braucht – auch hier mit den
Links-/Rechts-Seiten von Philosoph B. In die Nachricht steckt
Philosoph A außerdem sein eigenes Objekt.
Um ein Philosophen-Objekt zu konstruieren, machen wir eine kleine
Convenience-Funktion, die den Channel erzeugt:
let make_philosopher number =
{ number = number; channel = Domainslib.Chan.make_unbounded () }
Kommen wir nun zur eigentlichen Lebensführung der Philosophen bei
Tisch – diese erledigt die Funktion run_philosopher. Der geben wir
den „aktuellen“ Philosophen mit, den linken und den rechten Nachbarn,
sowie die Anfangszustände der beiden Hände:
let run_philosopher
(me: philosopher) (left_neighbor: philosopher) (right_neighbor: philosopher)
(left_hand: hand) (right_hand: hand) =
Jeder Philosoph befindet sich in einer Schleife, in der er die
Hände-Zustände mitführt. Außerdem merkt er sich, ob der linke oder
rechte Nachbar um eine Gabel gebeten hat:
let rec loop
(left_hand: hand) (right_hand: hand)
(wants_left: philosopher option) (wants_right: philosopher option) =
In jeder Runde von loop schauen wir erstmal, ob wir eine
Nachricht bekommen haben und bearbeiten diese gegebenenfalls:
match Domainslib.Chan.recv_poll me.channel with
| Some Die -> ()
| Some (Heres_fork Left) ->
loop Clean right_hand wants_left wants_right
| Some (Heres_fork Right) ->
loop left_hand Clean wants_left wants_right
| Some (Want_fork (who, Left)) ->
loop left_hand right_hand (Some who) wants_right
| Some (Want_fork (who, Right)) ->
loop left_hand right_hand wants_left (Some who)
Falls keine Nachricht anliegt, kümmern wir uns um die möglichen
Zustandskombinationen. Zunächst mal der Fall, wenn der Philosoph
beide Gabeln hat und deshalb essen kann:
| None ->
match (left_hand, right_hand, wants_left, wants_right) with
| (Clean, Clean, _, _) ->
loop Dirty Dirty wants_left wants_right
Wenn die linke Gabel schmutzig ist und der linke Nachbar sie will,
schickt der Philosoph sie ihm mit einer Heres_fork-Nachricht:
| (Dirty, _, Some left_philosopher, _) ->
begin
Domainslib.Chan.send left_philosopher.channel (Heres_fork Right);
loop No_fork right_hand None wants_right
end
Andersherum: Die rechte Gabel ist schmutzig und der rechte
Nachbar will sie:
| (_, Dirty, _, Some right_philosopher) ->
begin
Domainslib.Chan.send right_philosopher.channel (Heres_fork Left);
loop left_hand No_fork wants_left None
end
Jetzt fehlt noch die Gegenseite, wo dem Philosophen die linke oder
rechte Gabel fehlt – dann schickt der Philosoph eine
Want_fork-Anfrage an den entsprechenden Nachbarn:
| (No_fork, _, _, _) ->
begin
Domainslib.Chan.send left_neighbor.channel (Want_fork (me, Right));
loop Requested right_hand wants_left wants_right
end
| (_, No_fork, _, _) ->
begin
Domainslib.Chan.send right_neighbor.channel (Want_fork (me, Left));
loop left_hand Requested wants_left wants_right
end
Der Default macht einfach weiter in der Hoffnung, dass irgendwann eine
Nachricht kommt:
| _ -> loop left_hand right_hand wants_left wants_right
Schließlich müssen wir die loop-Schleife noch in einer neuen Domain
starten:
in Domain.spawn (fun _ -> loop left_hand right_hand None None)
Fertig! Also fast … so wie‘s ist, gibt‘s noch zwei Probleme:
- Philosophen sterben nie.
- Wir bekommen nicht mit, was sie tun.
Für‘s erste Problem können wir schonmal eine Funktion schreiben:
let kill (philosopher: philosopher) =
Domainslib.Chan.send philosopher.channel Die
Fürs zweite Problem wollen wir jeden Philosophen Meldung erstatten lassen,
wenn er isst. Man ist versucht, das mit Printf.printf zu machen -
da unser Programm mehrere Betriebssystem-Threads startet, würden die
Ausgaben aber durcheinanderkommen. Wir verschieben das Problem
erstmal und abstrahieren über einer Funktion print, die einen Text
ausdruckt. Das gibt uns Gelegenheit, die ganze
run_philosopher-Funktion nochmal im Zusammenhang abzudrucken:
let run_philosopher (print: string -> unit)
(me: philosopher) (left_neighbor: philosopher) (right_neighbor: philosopher)
(left_hand: hand) (right_hand: hand) =
let rec loop
(left_hand: hand) (right_hand: hand)
(wants_left: philosopher option) (wants_right: philosopher option) =
match Domainslib.Chan.recv_poll me.channel with
| Some Die -> ()
| Some (Heres_fork Left) ->
loop Clean right_hand wants_left wants_right
| Some (Heres_fork Right) ->
loop left_hand Clean wants_left wants_right
| Some (Want_fork (who, Left)) ->
loop left_hand right_hand (Some who) wants_right
| Some (Want_fork (who, Right)) ->
loop left_hand right_hand wants_left (Some who)
| None ->
match (left_hand, right_hand, wants_left, wants_right) with
| (Clean, Clean, _, _) ->
begin
print (Printf.sprintf "philosopher %d ate" me.number);
loop Dirty Dirty wants_left wants_right
end
| (Dirty, _, Some left_philosopher, _) ->
begin
Domainslib.Chan.send left_philosopher.channel (Heres_fork Right);
loop No_fork right_hand None wants_right
end
| (_, Dirty, _, Some right_philosopher) ->
begin
Domainslib.Chan.send right_philosopher.channel (Heres_fork Left);
loop left_hand No_fork wants_left None
end
| (No_fork, _, _, _) ->
begin
Domainslib.Chan.send left_neighbor.channel (Want_fork (me, Right));
loop Requested right_hand wants_left wants_right
end
| (_, No_fork, _, _) ->
begin
Domainslib.Chan.send right_neighbor.channel (Want_fork (me, Left));
loop left_hand Requested wants_left wants_right
end
| _ -> loop left_hand right_hand wants_left wants_right
in Domain.spawn (fun _ -> loop left_hand right_hand None None)
Um die print-Funktion zu realisieren, erledigen wir das Ausdrucken
in einer separaten Domain, der wir über einen Channel die zu
druckenden Texte übermitteln:
let start_print_domain () =
let chan = Domainslib.Chan.make_unbounded () in
let rec loop () =
let text = Domainslib.Chan.recv chan in
begin
Printf.printf "%s\n" text;
flush stdout;
loop ()
end
in
let domain = Domain.spawn (fun _ -> loop ()) in
(domain, fun text -> Domainslib.Chan.send chan text)
(Warum make_unbounded, fragen Sie vielleicht. Dazu gleich.)
Jetzt können wir die fünf Philosophen starten. Dabei müssen wir
darauf achten, dass die Zustände keinen Zyklus bilden – sonst werden
immer nur Gabeln herumgereicht und jeder hat immer nur eine. Darum
bekommt der erste Philosophen zwei Gabeln und der letzte keine:
let philosophers_5 () =
let (print_domain, print_text) = start_print_domain () in
let p1 = make_philosopher 1 in
let p2 = make_philosopher 2 in
let p3 = make_philosopher 3 in
let p4 = make_philosopher 4 in
let p5 = make_philosopher 5 in
let run = run_philosopher print_text in
let domain1 = run p1 p5 p2 Dirty Dirty in
let domain2 = run p2 p1 p3 No_fork Dirty in
let domain3 = run p3 p2 p4 No_fork Dirty in
let domain4 = run p4 p3 p5 No_fork Dirty in
let domain5 = run p5 p4 p1 No_fork No_fork in
()
Allerdings hat das Programm noch ein Manko: Es terminiert nicht.
Das ist im Philosophenproblem durchaus so angelegt, aber irgendwann
reicht‘s auch. Wir lösen das so, dass wir die print-Funktion
begrenzen, so dass sie nach einer bestimmten Anzahl von Ausgaben
Schluss macht:
let start_print_domain (n: int) =
let chan = Domainslib.Chan.make_unbounded () in
let rec loop (n: int) =
if n > 1
then
let text = Domainslib.Chan.recv chan in
begin
Printf.printf "%s\n" text;
flush stdout;
loop (n-1)
end
else ()
in
let domain = Domain.spawn (fun _ -> loop n) in
(domain, fun text -> Domainslib.Chan.send chan text)
Jetzt können wir darauf warten, dass die print-Domain fertig ist,
dann töten wir die ganzen Philosophen und warten, bis sie auch gestorben
sind:
let philosophers_5 () =
let (print_domain, print_text) = start_print_domain 1000 in
let p1 = make_philosopher 1 in
let p2 = make_philosopher 2 in
let p3 = make_philosopher 3 in
let p4 = make_philosopher 4 in
let p5 = make_philosopher 5 in
let run = run_philosopher print_text in
let domain1 = run p1 p5 p2 Dirty Dirty in
let domain2 = run p2 p1 p3 No_fork Dirty in
let domain3 = run p3 p2 p4 No_fork Dirty in
let domain4 = run p4 p3 p5 No_fork Dirty in
let domain5 = run p5 p4 p1 No_fork No_fork in
begin
Domain.join print_domain;
kill p1; kill p2; kill p3; kill p4; kill p5;
Domain.join domain1;
Domain.join domain2;
Domain.join domain3;
Domain.join domain4;
Domain.join domain5
end
Ach so: Ich wollte noch schreiben, warum der Puffer in
start_print_domain mit make_unbounded erzeugt wird: Nehmen wir an,
dass er es nicht ist – dann würden die print-Aufrufe der Philosophen
blockieren und sie kämen nie dazu, die Die-Nachricht zu verarbeiten.
Um es nochmal zusammenfassen:
- Seit Version 5.0 unterstützt OCaml Multicore-Programmierung.
- Existierende OCaml-Programme laufen unverändert, ohne
Performance-Verlust.
- OCaml unterstützt Parallelität mit Domains, die
Betriebssystem-Threads abbilden.
- Nebenläufigkeit und „Green Threads“ werden mit Hilfe von „effect
handlers“ unterstützt, zu denen wir noch separat schreiben werden.
Das war‘s jetzt aber – viel Vergnügen mit Multicore OCaml!