Vorschau:
Das „Dining-Philophers-Problem“ ist eine Parallelisierungsaufgabe aus der Informatik. Fünf Philosophen sitzen um einen Tisch mit für Tellern und fünf Gabeln dazwischen. Wenn einer von ihnen essen möchte, benötigt er beide Gabeln neben seinem Teller. By Benjamin D. Esham / Wikimedia Commons, CC BY-SA 3.0, https://commons.wikimedia.org/w/index.php?curid=56559 Damit können jeweils nur zwei Philosophen gleichzeitig essen und es muss jeweils ein Teller zwischen ihnen sein, an dem nicht gegessen wird. Eine historische Lösung des Problems kann man direkt in einer Publikation von Dijkstra nachlesen (S.29). Das hätte man einfach formalisieren können. Oder halt selbst nachdenken. In der Informatikwelt sind die Philosophen Prozesse, die um die Betriebssystemressourcen auf dem Tisch konkurrieren. Dabei muss man vermeiden, dass sich die Prozesse gegenseitig blockieren: Wenn alle gleichzeitig wollen, gibt es Streit und keiner kann die Ressourcen belegen, die er zum Essen braucht (informatisch: Verklemmung). Es darf aber auch keine Situation eintreten, in der alle so höflich sind, sich immer gegenseitig den Vortritt zu lassen (informatisch: Aushungerung). Und natürlich soll der Zugriff auf die Ressourcen fair und effizient sein. Die Herausforderung: Man „denkt“ beim Formalisieren nicht nur für einen Prozess, sondern für fünf, die miteinander in einer definierten Umgebung interagieren. Wer darf dann überhaupt miteinander essen? Um das zu formalisieren, nehmen wir mal eine simple minimale Datenstruktur – ein Feld mit einem booleschen Element für jeden Prozess – d.h. jeder hat sein Flag, dass er auf „ich will essen“ setzen kann. Dann gibt es fünf zulässige Konstellationen: 10100 10010 01010 01001 00101 Das ist schonmal...