Umfang

Dieses Thema eignet sich als Bachelorarbeit.

Empfohlene Vorkenntnisse

  • gute C Kenntnisse

Problem

Beim verteilten Model Checking gibt es eine Queue an Arbeitspaketen. Ein Arbeitspaket kann hier als Stück Speicher mit bekannter Länge verstanden werden. Sowohl die Länge der Queue als auch die Größe eines Arbeitspaketes kann je nach Modell sehr groß werden. Im Moment werden alle Arbeitspakete im Arbeitsspeicher gehalten.

Damit der RAM nicht vollläuft und auf Festplatte geswappt wird, sollen Arbeitspakete nach einfachen Kriterien auf Festplatte geschrieben und von der Festplatte auch wieder gelesen werden.

Minimalanforderungen

  • Implementierung einer disk-backed Queue in C:
    • Es sind maximal 100 Arbeitspakete gleichzeitig im Speicher.
    • Wird auf ein Element der Queue zugegriffen, das nicht im Speicher liegt, so sollen so viele Pakete wie möglich geladen werden, bis 100 oder alle Pakete im Speicher sind.
    • Das Speichern kann in einer Datei pro Arbeitspaket geschehen.
  • Eine sinnvolle Simulation zum Testen ist implementiert.

Variationen

  • Asynchrones Laden / Schreiben
  • Implementierung eines zirkulärer Buffers in einer einzelnen Datei
  • Verwendung von memory-mapped Dateien

Kontakt

Philipp Körner
Raum 25.12.02.56
p.koerner@hhu.de