Algorithmus Warteschlange Ringpuffer wirklich fehlerfrei

[Barista]

Ich hatte Bedarf an einer Warteschlange, aufgebaut mit einem Array als Ringpuffer.

Wegen Speicher und Performance wollte ich keine vorgefertigte Java-Collection verwenden, weil da für primitive Typen meist Wrapper-Objekte notwendig sind.

Klar, dass man zuerst mal eine Suchmaschine benutzt.

Bei den gefundenen Lösungen hat mich gestört, dass keine oder zu wenig Tests dabei waren.

Ausserdem, selbst gekocht schmeckt besser.

GitHub - HeinerKuecker/Array-Ringbuffer-Queue-Java: A queue based on a ringbufferr, which in turn is based on a array

A queue based on a ringbufferr, which in turn is based on a array - HeinerKuecker/Array-Ringbuffer-Queue-Java

github.com

Das Problem beim Ringpuffer ist, dass man anhand der beiden Indexwerte zum Hinzufügen und zum Entnehmen nicht erkennen kann, ob bereits ein Überlauf erfolgte oder ob der noch kommt.

Nach einigem Rumprobieren bin ich auf dem Nachhauseweg auf folgende Lösung gekommen:

Ich führe beim Array-Zugriff immer ein Modulo auf den jeweiligen Index aus.

Dadurch bleibe ich sicher in den Array-Grenzen.

Ich lasse den Hinzufüge-Index über die Array-Grenze laufen, ist kein Problem wegen dem Modulo beim Zugriff.

So ist der Hinzufüge-Index immer größer als der Entnehm-Index.

Wenn auch der Entnehm-Index die Array-Grenze (0 bis Array-Größe - 1) verlässt, reduziere ich beide Indexe auf den Array-Bereich (Modulo).

Ich bewege mich also auf dem Zahlenstrahl ein Stück weiter, bleibe aber aufgrund des Modulo im Bereich des Arrays.

Das hat auf Anhieb geklappt und alle Tests waren grün.

In der Code-Coverage konnte ich sehen, dass einige Codezeilen zum Abfragen und Reduzieren nie benutzt wurden, die konnte ich entfernen.

Den alten Code (Zwischenstand) habe ich mit ins Repo eingecheckt.

Ich nehme an, dass meine Tests recht gut sind.

Es bleibt aber immer noch die Angst, dass ein Fehler drin ist.

Ich wäre sehr dankbar, wenn jemand einen Fehler entdeckt oder mir einen Hinweis gibt, wie ich die Fehlerfreiheit beweisen kann.

Danke

 

[mihe7]

wie ich die Fehlerfreiheit beweisen kann.

Mit einem formalen Korrektheitsbeweis, der aber alles andere als trivial ist.

Das Problem beim Ringpuffer ist, dass man anhand der beiden Indexwerte zum Hinzufügen und zum Entnehmen nicht erkennen kann, ob bereits ein Überlauf erfolgte oder ob der noch kommt.

Nehmen wir mal head und tail für die Indizes. Wenn Du als Invariante nimmst, dass für einen leeren Puffer head == tail gilt, musst Du dafür sorgen, dass head != tail gilt, wenn der Puffer nicht-leer ist.

Gehen wir von einem leeren Puffer mit n Elementen aus, gilt head == tail und ganz offensichtlich (head+n) % n == tail. Damit das nicht passiert, darfst Du max n-1 Elemente einfügen. Dann entsteht ein Überlauf, wenn (head + 1) % n == tail.

Sprich: Du musst einfach für ein Element mehr Platz schaffen.

Alternativ kannst Du als Invariante nehmen, dass im Fall von head == tail der Puffer entweder leer oder voll ist. Dann musst Du den Fall auf andere Weise unterscheiden, z. B. mit einem boolean oder indem Du die Zahl der Elemente speicherst.

Mehr fällt mir dazu spontan auch nicht ein.

 

[Barista]

Gehen wir von einem leeren Puffer mit n Elementen aus, gilt head == tail und ganz offensichtlich (head+n) % n == tail. Damit das nicht passiert, darfst Du max n-1 Elemente einfügen. Dann entsteht ein Überlauf, wenn (head + 1) % n == tail.

Ja, so müsste ein Beweis aufgebaut sein.

Sprich: Du musst einfach für ein Element mehr Platz schaffen.

Das trifft nicht zu, alle Speicherplätze sind verwendbar.

Alternativ kannst Du als Invariante nehmen, dass im Fall von head == tail der Puffer entweder leer oder voll ist. Dann musst Du den Fall auf andere Weise unterscheiden, z. B. mit einem boolean oder indem Du die Zahl der Elemente speicherst.

Durch die Modulo-Operation hat die Einfüge-Position einen Merker für den Überlauf.

Es wäre schön, wenn man den Beweis der Korrektheit automatisiert prüfen könnte, also dass er nach Programmänderungen immer noch eingehalten ist. Dies geht sicher nur mit statischer Codeanalyse.

Vielen Dank

 

[httpdigest]

Dinge werden sehr viel einfacher, wenn man nicht eine read- und write-Position speichert, sondern eine read-Position und die Länge/Anzahl der aktuellen Elemente. Das verhindert, dass man den durch die Modulo-Operation mehrdeutigen Fall read==write (mod n) (voll oder leer?) bekommt.

import java.util.*;
public class IntRingBuffer {
  private int read;
  private int len;
  private final int[] arr;
  public IntRingBuffer(int capacity) {
    this.arr = new int[capacity];
  }
  public int capacity() {
    return arr.length;
  }
  public boolean isEmpty() {
    return currentSize() == 0;
  }
  public boolean isFull() {
    return currentSize() == capacity();
  }
  public int currentSize() {
    return len;
  }
  public int freeSize() {
    return capacity() - currentSize();
  }
  public boolean add(int v) {
    if (isFull())
      return false;
    arr[(read + len++) % capacity()] = v;
    return true;
  }
  public int get() throws NoSuchElementException {
    if (len == 0)
      throw new NoSuchElementException();
    return arr[read];
  }
  public int take() throws NoSuchElementException {
    if (len == 0)
      throw new NoSuchElementException();
    int res = arr[read];
    read = (read + 1) % capacity();
    len--;
    return res;
  }
}

 

[mihe7]

Das trifft nicht zu, alle Speicherplätze sind verwendbar.

Natürlich sind alle Speicherplätze verwendbar, aber nicht mit zwei Indizes, da head == tail sowohl in einem leeren als auch in einem vollen Puffer gilt.

Durch die Modulo-Operation hat die Einfüge-Position einen Merker für den Überlauf.

Der Modulo dient für einen anderen Überlauf, nämlich den über die Arraygrenze. Der Überlauf des Puffers wäre gegeben, wenn in einen vollen Puffer eingefügt werden würde und hat mit dem Modulo nichts zu tun. Die Situation lässt sich mit zwei Indizes nicht von einem leeren Puffer unterscheiden, wenn alle Speicherplätze verwendet werden; wohl aber mit einem Index und der Zahl der Elemente im Puffer.

 

[Barista]

Dinge werden sehr viel einfacher, wenn man nicht eine read- und write-Position speichert, sondern eine read-Position und die Länge/Anzahl der aktuellen Elemente. Das verhindert, dass man den durch die Modulo-Operation mehrdeutigen Fall read==write (mod n) (voll oder leer?) bekommt.

Ja, so geht es auch.

Vielen Dank

 

[temi]

  public boolean add(int v) {
    if (isFull())
      return false;

Ich war immer der Ansicht, dass ein Ringpuffer gar nicht "voll" sein kann, weil er ja, wie der Name "Ring" schon aussagt, den ältesten Inhalt wieder überschreibt?

 

[mihe7]

Ich war immer der Ansicht, dass ein Ringpuffer gar nicht "voll" sein kann, weil er ja, wie der Name "Ring" schon aussagt, den ältesten Inhalt wieder überschreibt?

= Queue mit maximaler Größe.

 

[Barista]

Ich war immer der Ansicht, dass ein Ringpuffer gar nicht "voll" sein kann, weil er ja, wie der Name "Ring" schon aussagt, den ältesten Inhalt wieder überschreibt?

Das ist sicher eine Frage der Definition, in meinem Fall ist Überschreiben nicht gewünscht.