2. Feb

Die technischen Informationen (zu Kitty und CAT) sind noch vorläufig.

20. Apr

Das Kickoff-Meeting findet am Donnerstag, den 23. April, um 13:00Uhr statt.

21. Apr

Die SEP eigene Projektseite ist hier online. Die technischen Details wurden finalisiert.

22. Apr

Die fehlenden Abschnitte in Teil 2 wurden ergänzt.

Das diesjährige Softwareentwicklungsprojekt des Instituts für Theoretische Informatik (TCS) beschäftigt sich mit der hardwarenahen Verifikation. Genauer soll ein Tool entwickelt werden, welches Assembler-Programme für eine gegebene Prozessorarchitektur analysiert. Dabei sind sowohl das zu verifizierende Assembler-Programm als auch eine formale Beschreibung der Prozessorarchitektur Eingaben des zu entwickelnden Tools.

Inhaltsverzeichnis:

• Motivation
• Kitty-Assembler-Programme (CPU-Simulator Teil 1)
• Von Kitty zu Eventgraphen (CPU-Simulator Teil 2)
• CAT als formale Beschreibung von Prozessorarchitekturen (CPU-Simulator Teil 3)
• Identifizieren erlaubter Ausführungen (CPU-Simulator Teil 4)
• Korrektheitstest (CPU-Simulator Teil 5)
• Aufgabenstellung
• Resourcen
• Technischer Spielrahmen
• Betreuer

Bei der Entwicklung sicherheitskritischer Software und Software für den Finanzsektor wird besonderes Augenmerk auf die Qualitätssicherung gelegt, da Fehler (Bugs) hier zu schweren Personen- und Sachschäden führen können. Ein großes Problem bei der Qualitätssicherung stellt allerdings die Komplexität heutiger Computersysteme dar. Zum einen werden Programme in Hochsprachen geschrieben, danach automatisch kompiliert und der resultierende Assembler-Code ausgeführt. Zum anderen integrieren Prozessoren beim Ausführen von Assembler-Code viele Optimierungen. Zusammen führt dies dazu, dass Programmierende zumeist nicht wissen (können) was genau im Prozessor passiert, wenn sie ihren Code ausführen.

Im diesjährigen SEP wollen wir die durch Hardwareoptimierungen entstehenden Probleme aufdecken und Programmierenden eine Möglichkeit geben diese zu erkennen bzw. zu verstehen. Dazu soll ein CPU-Simulator entwickelt werden, welcher alle durch eine gewisse Prozessorarchitektur erlaubten Ausführungen berechnet. In der Tat, selbst wenn das auszuführende Assembler-Programm deterministisch ist, weisen moderne Prozessoren durch oben genannte Optimierungen nicht-deterministisches Verhalten auf. Dies führt in der Praxis oft zu Fehlern, insbesondere wenn sich Programmierende der Problematik nicht bewusst sind.

Die oben beschriebene Problematik wird dadurch verschärft, dass jede Prozessorarchitektur (x86, amd64, arm, ...) stark unterschiedliche Optimierungen integriert/erlaubt. Aus diesem Grund soll der zu entwickelnde CPU-Simulator nicht für eine a priori gewählte Prozessorarchitektur implementiert werden, sondern die Prozessorarchitektur soll frei wählbar sein. In Forschung und Praxis wird hierzu eine relationale Beschreibung von Prozessorarchitekturen verwendet, die unser CPU-Simulator ebenfalls nutzen soll.

Beispiel Im folgenden erörtern wir die Unterschiede zwischen verschiedenen Prozessorarchitekturen an einem Beispiel. Wir betrachten Dekker's Mutex, ein Locking-Verfahren, welches zwei Threads erlaubt Code unter wechselseitigem Ausschluss auszuführen:

// globale Variablen
bool flag0 = false;
bool flag1 = false;
int turn = 0;


// Thread 0                                 // Thread 1
flag0 = true;                               flag1 = true;
while (flag1) {                             while (flag0) {
    if (turn != 0) {                            if (turn != 1) {
        flag0 = false;                              flag1 = false;
        while (turn != 0) {}                        while (turn != 1) {}
        flag0 = true;                               flag1 = true;
    }                                           }
}                                           }
// wechselseitiger Ausschluss (*)           // wechselseitiger Ausschluss (*)
turn = 1;                                   turn = 0;
flag0 = false;                              flag0 = false;

Unser Bestreben ist es, nachzuweisen, dass dieser Algorithmus tatsächlich wechselseitigen Ausschluss garantiert. D.h. wir wollen nachweisen, dass Thread0 und Thread1 nicht gleichzeitig den mit (*) markierten Bereich betreten können.

Sequential Consistency (SC) Intuitiv ist die gewünschte Eigenschaft erfüllt. Um nun aber ein Korrektheitsargument anzuführen, werden wir folgende, sinnvolle Annahme treffen müssen: die von den Threads gelesenen Werte sind diejenigen, die zuletzt geschrieben wurden—unabhängig davon, welcher Thread den jeweils letzten Wert geschrieben hat. Dieses Verhalten wird in der Literatur als Sequential Consistency (SC) bezeichnet, da Anweisungen in der Reihenfolge sichtbar sind, in der sie ausgeführt werden.

Total Store Ordering (TSO) In der Praxis findet SC allerdings keine Anwendung. Moderne Desktop-Prozessoren (x86, amd64) der bekannten Hersteller implementieren eine wesentlich schwächere Garantie: das sogenannte Total Store Ordering (TSO). Hier wird jeder Prozessor mit einem lokalen Write-Buffer versehen. Schreiboperationen werden in diesem Write-Buffer zwischengespeichert und erst später in den Hauptspeicher geschrieben. Eine Konsequenz dieser Optimierung ist Folgende: Schreibanweisungen wie Variablenupdates werden nicht sofort synchronisiert. D.h., es ist nicht garantiert, dass die zuletzt geschriebenen Werte auch tatsächlich für einen Thread sichtbar sind. Unglücklicherweise führt dies in Dekker's Mutex dazu, dass wechselseitiger Ausschluss nicht garantiert ist.

Im Falle von TSO sagen wir, dass das Programm nicht ausreichend synchronisiert ist. Um solche Probleme zu beheben, führen TSO-Prozessoren sogenannte Fences ein—Anweisungen, die den Prozessor zur Laufzeit dazu zwingen, den lokalen Write-Buffer zu leeren.

Der zu entwickelnde CPU-Simulator soll dabei helfen, Probleme mit mangelnder Synchronisation ausfindig zu machen. Zum einen soll er alle Programm-Ausführungen berechnen und so aufzeigen, dass eine TSO-Ausführung existiert, bei der der wechselseitige Ausschluss verletzt wird. Zum anderen erlaubt ein Vergleich der SC- und TSO-Ausführungen zu erkennen, dass Fences benötigt werden, um gewisse TSO-Ausführungen zu verbieten.

Die zu analysierenden Programme liegen in der Instituts-eigenen Assembler-Sprache Kitty vor. Wir nehmen hier vereinfachend an, dass alle Prozessorarchitekturen diese Assembler-Sprache benutzen. In der Praxis ist dies nicht der Fall: Prozessorarchitekturen unterscheiden sich nicht nur in ihrem Verhalten, sondern auch in ihrer Assembler-Sprache.

Kitty ist durch folgende EBNF definiert:

Prog     ::=  RegDecl* LocDecl* Init? Proc+ Check?
RegDecl  ::=  'register' NAME ';'
LocDecl  ::=  'location' NAME ';'
Proc     ::=  'process' INT '{' Stmt* '}'
Stmt     ::=  Lab? Com ';'
Lab      ::=  NAME ':'
Com      ::=  Reg ':=' Immi |  Reg ':=' Reg | Reg ':=' Loc 
           |  Loc ':=' Immi | Loc ':=' Reg 
           |  'swap' '(' Loc ',' Reg ')' | 'goto' NAME 
           |  'jumpc' Reg NAME | 'mfence' | 'sfence' | 'lfence'
Reg      ::=  '%' NAME
Loc      ::=  '[' NAME ']'
Immi     ::=  '$' INT
Init     ::=  '@init' '{' (INT ':' Reg ':=' Immi | Loc ':=' Immi)* '}'
Check    ::=  '@check' '{' ('exists' | 'forall') Cond '}'
Cond     ::=  'true' | 'false' | INT ':' Reg '=' Immi | Loc '=' Immi
           |  '(' Cond ')' '&&' '(' Cond ')'  
           |  '(' Cond ')' '||' '(' Cond ')' | '!' '(' Cond ')'

Ein Kitty-Programm besteht also aus beliebig vielen (ggf. keinen) Registerdeklerationen (RegDecl*), beliebig vielen (ggf. keinen) benannten Speicherzellen (LocDecl*), einer optionalen Initialisierung (Init?), einem oderer mehreren Prozessen (Proc+) und einem optionalem Test (Check?).

Register sind Prozess-lokal, d.h. jeder Prozess hat seine eigene Kopie eines jeden deklarierten Registers. Des Weiteren kann ein Prozess nicht auf die Register anderer Prozesse zugreifen, weder lesend noch schreibend. Speicherzellen sind dageben global, für alle Prozesse lesbar und schreibbar.

Jeder Kitty-Prozess hat eine eindeutige, ganzzahlige Identifikationsnummer und besteht aus beliebig vielen (ggf. keinen) Statements (Stmt*). Ein Statement hat ein optionales Label (Lab?) und besteht aus einem Command (Com). Die Commands sind:

• Reg ':=' Immi:  Zuweisung an ein Register von einem konstanten Wert.
• Reg ':=' Reg:  Zuweisung an ein Register von einem Register.
• Reg ':=' Loc:  Zuweisung an ein Register von einer Speicherzelle.
• Loc ':=' Immi:  Zuweisung an eine Speicherzelle von einem konstanten Wert.
• Loc ':=' Reg:  Zuweisung an eine Speicherzelle von einem Register.
• 'swap' '(' Loc ',' Reg ')':  Atomarer Tausch des Inhalts von Speicherzelle und Register.
• 'goto' NAME:  Sprung an das Label mit namen NAME.
• 'jumpc' Reg NAME:  Konditionaler Sprung an das Label mit Namen NAME falls der Registerinhalt von Reg ungleich $0.
• 'mfence', 'sfence', 'lfence':  Synchronization durch verschiedene Fences (memory, store, load).

Wir nehmen an, dass Namen NAME in Kitty-Programmen nicht überladen werden. D.h., die Namen von Registern, Speicherzellen und Labels sind verschieden und entsprechen nicht den reservierten Keywords.

Speicherzellen und Register werden default-initialisiert mit dem Wert $0. Um dieses Verhalten zu beeinflussen, kann eine Initialisierung angegeben werden. In dieser Initialisierung kann der Inhalt von Speicherzellen und Registern ähnlich zu den Zuweisungen in Prozessen gesetzt werden. Da die Initialisierung Prozess-übergreifend ist, müssen Register allerdings mit dem jeweiligen Prozess geprefixt werden. Zum Beispiel bedeutet 1:%reg := 77, dass das Register %reg des Prozess mit ID 1 auf den Wert 77 gesetzt wird.

Tests erlauben existenziell- und allquantifizierte Bedingungen an Ausführungen zu stellen. Die Bedingungen enthalten die üblichen Boolschen Operatoren und können den Inhalt von Registern und Speicherzellen mit konstanten Werten vergleichen. Ähnlich zur Initialisierung, müssen Register mit einer Prozess-ID geprefixt werden.

Neben den oben erwähnten Konstrukten, nehmen wir an, dass Zeilenkommentare wie in C/Java üblich mit // eingeleitet werden.

Wir können nun Dekker's Mutex von oben in Kitty übersetzen (Stichwort Code Obfuscation):

// benannte Speicherzellen
register tmpFlag;
register tmpTurn;
location flag0; // mit $0 initialisiert
location flag1; // mit $0 initialisiert
location turn; // mit $0 initialisiert


// Prozess 0                       // Prozess 1
[flag0] := $1;                     [flag1] := $1;
%tmpFlat := [flag1];               %tmpFlat := [flag0];
jumpc %tmpFlat loop1;              jumpc %tmpFlat loop2;
goto critical1;                    goto critical2;
                                   
loop1:                             loop2:
%tmpTurn := [turn];                %tmpTurn := [turn];
jumpc %tmpTurn inner1;             jumpc %tmpTurn loop2;
goto loop1;                        goto inner2;
inner1:                            inner2:
[flag0] := $0;                     [flag1] := $0;
wait1:                             wait2:
%tmpTurn := [turn];                %tmpTurn := [turn];
jumpc %tmpTurn wait1;              jumpc %tmpTurn continue2;
[flag0] := %1;                     goto wait2;
                                   continue2:
critical1:                         [flag1] := %1;
...                                
[turn] := $1;                      critical2:
[flag0] := $0;                     ...
                                   [turn] := $1;
                                   [flag0] := $0;

Betrachte das folgende Programm, geschrieben in Kitty:

register ret;
location x;
location y;


process 1 {                       process 2 {
    c1: [x] := $1;                    d1: [y] := $1;
    c2: %ret := [y];                  d2: %ret := [x];
}                                 }


@check: { exists  1:%ret = $0  &&  2:%ret = $0 }

Der Check am Ende des Programms fragt, ob es eine Ausführung gibt, sodass die beiden Register 1:%ret und 2:%ret am Ende der Ausführung den Inhalt $0 haben. Um solche Fragen unter einem gegebenen Speichermodell zu beantworten, müssen wir das Programm zunächst in ein geeignetes mathematisches Modell übersetzen. Hierzu nutzen wir sogenannte Eventgraphen.

Ein Event beschreibt, um welche Art von Speicherzugriff es sich bei einer Instruktion im Programm handelt. Es gibt Write-Events und Read-Events. Erstere haben die Form o = wr(x,v), wobei x eine Speicherzelle ist und v der Wert, der in die Zelle geschrieben wird. Read-Events o = rd(x,y) geben an, welchen Wert v sie aus der Speicherzelle x lesen. Aus obigem Beispiel können wir sechs Events ableiten. Jeder Ablauf des Programms genügt dann folgendem Graphen:

Beachte, dass die initialen Events i1 und i2 dazu dienen, die Speicherzellen x und y zu initialisieren. Die beiden Schreibzugriffe des Programms, auf die Zellen x und y, werden durch die Events c1 und d1 modelliert. Die Lesezugriffe werden durch c2 und d2 dargestellt. Die Kanten im Graph modellieren den Kontrollfluss des Programms. Zunächst werden die Speicherzellen initialisiert, dann wird der Kontrollfluss der Prozesse eingehalten. Diese Kontrollflussrelation nennt man Program Order, abgekürzt po.

Es ist vor der Ausführung des Programms nicht klar, welche Werte in den Registern 1:%ret und 2:%ret gespeichert werden. Wir wissen zu diesem Zeitpunkt nur, dass die Werte in den Registern von einem Schreibzugriff auf x bzw. y stammen. Jedoch ist nicht bekannt, welcher Schreibzugriff dies genau ist. Diese Mehrdeutigkeit wird im Graphen durch Einführen einer neuen Relation behoben.

Die Reads From Relation, geschrieben rf, modelliert, woher die Werte der Lesezugriffe stammen und welche Werte die Zugriffe lesen. Wenn wir in obigem Programm alle Ausführungen betrachten, gibt es insgesamt vier Möglichkeiten. Diese werden im Folgenden aufgeführt—die Reads From Relation ist hierbei jeweils rot markiert.

Im allgemeinen gilt, dass der gelesene Wert v eines Read-Events o = rd(x,v) immer der Wert des Write-Events o' = wr(x,v) ist, welches zu o mit rf in Beziehung steht. Zudem gibt es für jedes Read-Event o genau ein solches Write-Event o'.

Abhängige Write-Events

In obigem Beispiel sind die geschriebenen Werte der Write-Events aus dem Code des Kitty-Programms direkt ersichtlich. Es ist schon vor der Ausführung des Programms klar, dass die Events c1 und d1 jeweils den Wert $1 schreiben. Dies liegt daran, dass der Befehl c1: [x] = $1 eine Zuweisung eines festen Werts ist. Die Syntax von Kitty erlaubt jedoch auch Zuwesiungen der Form dep: [x] = %reg. Hier wird der Speicherzelle x der aktuelle Inhalt des Registers %reg zugewiesen. Da der Inhalt des Registers von einem Schreibzugriff/Write-Event abhängen kann, trifft dies auch auf den Schreibzugriff dep zu. Betrachte dazu folgendes Programm:

register temp;
location x;
location y;

process 1: {                   process 2: {
    a1: [x] = $1;                  a2: %temp = [x];
}                                  dep: [y] = %temp;
                               }

Es ergibt sich, wie im Beispiel oben, folgender vorläufiger Event-Graph. Beachte, dass wir den Wert des Write-Events dep zum jetzigen Zeitpunkt nicht kennen. (Vereinfachend ignorieren wir hier das initiale Write auf y.)

Das Write-Event dep muss laut Programm-Code jenen Wert v in y schreiben, welcher vom Read-Event a2 aus x gelesen wird. Dieser Wert ist jedoch nicht fest. Er hängt davon ab, aus welchem Schreibzugriff (i oder a1) das Read-Event a2 liest. Es ergeben sich daher folgende Eventgraphen:

Das Beispiel verdeutlicht, dass die Werte der Write-Events von Read-Events abhängen können. Dies muss man beachten, wenn man algorithmisch alle Eventgraphen aufbaut. Beim Aufbauen müssen wir uns daher immer die aktuell möglichen Werte der Register/Read-Events merken, um alle Ausführungen zu erhalten.

Jumps

Die Sprache Kitty erlaubt goto- und jumpc-Anweisungen. Wir zeigen an einem Beispiel, wie sich solche Anweisungen in einen Event-Graphen übersetzen lassen.

register temp;
location x;

@init { [x] := $1 }

process 1: {                         process 2: {
    a1: %temp := [x];                    b: [x] := $0;
    a2: jumpc %temp a1;              }
}

Obiges Programm hat den konditionalen Sprung: a2: jumpc %temp a1. Dieser testet, ob im Register %temp ein Wert ungleich $0 steht und springt dann zum Label a1. Andernfalls stoppt der Prozess die Ausführung. Da Speicherzelle x mit $1 initialisiert wird, kann nur das Ausführen des zweiten Prozesses der Zelle den Wert $0 zuweisen—also den Sprung verhindern. Bis zu dieser Ausführung kann der erste Prozess den Sprung beliebig oft ausführen. Da wir nicht wissen, wann der zweite Prozess seine Ausführung beginnt, kann eine Ausführung des Programms beliebig lang sein.

Im Eventgraphen wird dieses Verhalten durch das Einführen von Eventkopien modelliert. Wenn der erste Prozess den Sprung i-mal ausführt, benötigen wir i Kopien von a1, eine für jede Iteration. Der Sprung selbst wird nicht durch ein Event dargestellt, da es sich nicht um einen Speicherzugriff handelt. Es wird lediglich ein Registerinhalt mit einem konstanten Wert verglichen. Eventgraphen für obiges Programm genügen dann folgender Form:

Das Event a1(0) modelliert den Speicherzugriff a1 bevor der Sprung ausgeführt wurde. Die Ausführung von a1 nachdem der Prozess einen Sprung gemacht hat wird durch das Event a1(1) dargestellt. Folglich modelliert a1(2) die Ausführung von a1 nach zwei Sprüngen, usw. Nach i vielen Sprüngen ist a1(i) schließlich die letzte Ausführung von a1. Beachte, dass hier $0 gelesen wird. Dies bedeutet, dass der zweite Prozess den Inhalt der Zelle x geändert hat und kein weiterer Sprung erfolgt.

Wie oben erwähnt, kann der erste Prozess beliebig viele Sprünge machen, bevor der zweite Prozess interveniert. Dies führt dazu, dass Eventgraphen beliebig lang werden können. Zudem gibt es unendlich viele Graphen—einen für jede Ausführung unterschiedlicher Länge. Diese können wir nicht alle analysieren. Um dieses Problem zu umgehen, beschränkt man die Größe der Eventgraphen, die man betrachten möchte. Man führt eine obere Schranke für die Anzahl der Events ein und betrachtet nur solche Graphen, die weniger (oder gleich viele) Events haben. Intuitiv setzt man damit ein Limit an die Länge der Ausführungen des Programms, die man analysiert. Als Vorteil ergibt sich, dass es nur endlich viele dieser Ausführungen und Eventgraphen gibt. Jedoch muss klar sein, dass die eingeführte Schranke eine Unterapproximation an das Programmverhalten (alle Ausführungen) darstellt.

Nehmen wir an, im obigen Beispiel setzn wir das Limit auf vier Events pro Ausführung. Dann können wir die folgenden beiden Event-Graphen ableiten:

Der Graph links zeigt eine Ausführung, bei welcher der zweite Prozess der Speicherzelle x den Wert $0 zuweist, bevor der konditionale Sprung im ersten Prozess ausgeführt wird. Der Graph auf der rechten Seite zeigt eine Ausführung, bei welcher der konditionale Sprung einmal ausgeführt wurde, bevor der zweite Prozess der Zelle x den Wert $0 zugewiesen hat. Nach dieser Zuweisung führt der erste Prozess seine Ausführung fort, stoppt dann aber beim zweiten konditionalen Sprung, da das Register temp nun den Wert $0 enthält.

Bei der Konstruktion der Eventgraphen für ein Programm mit dem Command jumpc müssen wir also eine Schranke an die Anzahl der Events beachten. Analog verhält es sich mit einem goto und wenn mehrere dieser Commands auftreten. Man spricht in diesem Zusammenhang von Unrolling, da wir die Sprünge bis zu einer gewissen Tiefe ausrollen.

Swaps

Wir betrachten folgendes Kitty-Programm, welches das swap Command benutzt.

register EAX;
location x;

@init {
  [x] := $1
  EAX := $2
}

process 1: {                      process 2: {
  a: swap([x],%EAX);                  b: [x] := $0;
}   

Das Command a: swap([x],%EAX) tauscht den Inhalt der Speicherzelle x und des Registers %EAX aus. Die Ausführung von a: swap([x],%EAX) entspricht also dem Ausführen folgender Sequenz von Commands: %tmp := %EAX; %EAX := [x]; [x] := %tmp, wobei tmp ein Behelfsregister ist. Diese Sequenz macht deutlich, dass es beim Ausführen von swap zu einem Lesezugriff und zu einem Schreibzugriff auf Speicherzelle x kommt. Wir modellieren diese Zugriffe in Eventgraphen durch separate Events. Für obiges Programm erhalten wir dann die folgenden Graphen, in welchen die Speicherzugriffe von obigem swap durch a1 und a2 modelliert sind:

Wir stellen fest, dass wir anhand der Events nicht unterscheiden können, ob das Command swap([x],%EAX) oder die Sequenz %tmp := %EAX; %EAX := [x]; [x] := %tmp ausgeführt wurde. Dies widerspricht unserer Vorstellung von swap: wie in Teil 1 beschrieben, ist die intendierte Semantik von swap das atomare Austauschen. Jedoch ist diese Mehrdeutigkeit vom Eventgraphen gewollt! Ob swap atomar ausgeführt wird oder nicht hängt nämlich nicht von der Syntax (also der Tatsache, dass wir das Command swap genannt haben) ab, sondern von der Prozessorarchitektur. Wie die Prozessorarchitektur schließlich mit swap umgeht, können wir an dieser Stelle nicht klären—wir verweisen auf Teil 3.

Damit zwischen swap und der Sequenz unterschieden werden kann, werden wir in Teil 3 eine Relation rmw einführen. Diese zeigt auf, welche Events in einem Eventgraphen zu einer atomaren Operation wie swap gehören. In unserem Beispiel fügen wir eine rmw-Kante von a1 nach a2 ein. Zur besseren Übersicht sind die Kanten der Relationen mit ihrem jeweiligen Namen markiert.

Damit der CPU-Simulator für frei konfigurierbare Prozessorarchitekturen funktioniert, verwenden wir die Sprache CAT. CAT erlaubt es uns Relationen über den Events des Eventgraphen einer Programmausführung zu definieren. Zusätzlich können Bedingungen an die definierten Relationen gestellt werden (z.B. Kreisfreiheit), um die erlaubten Ausführungen einzuschränken.

Folgende EBNF definiert CAT:

Arch  ::=  (Incl | Def | Chk | Act)*
Incl  ::=  'include' '"' FILE '"'
Def   ::=  'let' NAME ':=' Rel | 'let rec' NAME ':=' Rel
Rel   ::=  NAME | NAME * NAME | '( 'Rel ')' | Rel '+' | Rel '*' | Rel '^-1' 
        |  Rel ';' Rel | Rel '|' Rel | Rel '&' Rel | Rel '\' Rel
Chk   ::=  'acyclic' NAME | 'irreflexive' NAME | 'empty' NAME
Act   ::=  'show' NAME

Ein CAT-File zur Definition eines Prozessormodells besteht also aus einer Folge von Anweisungen mit folgender Bedeutung:

• Komponente Incl:

  Läd ein CAT-File. Intuitive soll die include Anweisung mit dem Inhalt der angegebenen Datei ersetzt werden.

• Komponente Def:

  Definiert eine neue Relation. Der Name der neuen Relation ist durch NAME gegeben und kann nachfolgend im CAT-File verwendet werden. Es gibt zwei verschiedene Arten von Definitionen: rekursive (let rec) und nicht-rekursive (let). Die meisten Relationen sind nicht rekursiv, d.h. sie werden durch einen Relationen-Ausdruck definiert in dem die neu zu definierende Relation nicht vorkommt. Bei rekursiven Definition dagegen darf die neu definierte Relation bereits im definierenden Relationen-Ausdruck vorkommen. Wir meinen dann diejenige Relation, welche dem kleinsten Fixpunkt der Definitionsvorschrift entspricht.

• Komponente Rel:

  Liefert eine Relation. Relationen sind bereits existierende Relationen (NAME) oder das kartesische Produkt zweier Eventmengen (NAME * NAME). Ferner stehen die folgenden Operationen auf Relationen zur Verfügung: Klammern ('(' Rel ')'), transitiver Abschluss (Rel '+'), transitiv-reflexiver Abschluss (Rel '*'), Invertieren (Rel '^-1'), sequentielle Komposition (Rel ';' Rel), Vereinigung (Rel '|' Rel), Schnitt (Rel '&' Rel) und Differenz (Rel '\' Rel).
  Es gilt zu beachten, dass es Basisrelationen gibt, welche immer definiert sind — auch ohne eine entsprechende Def im CAT-File. Ebenso gibt es feste Eventmengen. Sie dienen dazu, mittels (Def) komplexere Relationen zu definieren. Die Basisrelationen und Eventmengen werden weiter unten aufgeführt und beschrieben.

• Komponente Chk:

  Stellt eine Anforderung and die gegebene Relation (NAME). Die Anforderungen sind Kreisfreiheit (acyclic), Irreflexivität (irreflexive) und Leerheit (empty). Irreflexivität bedeutet, dass kein Element existiert, welches mit sich selbst in Relation steht. Beachte, dass Kreisfreiheit einer Relation r geprüft werden kann, indem man Irreflexivität von r+ prüft.

• Komponente Act:

  Instruktion, welche die visuelle Ausgabe von Relationen beeinflusst. Es sollen nur solche Relationen angezeigt werden, die in show vorkommen.

Sei Evt die Menge aller Events im betrachteten Eventgraphen. Dann sind die in CAT verfügbaren Eventmengen wie folgt definiert:

CAT definiert folgende Basisrelationen, wobei Evt wie oben:

Die Relationen data und ctrl sind optional, siehe Aufgabenstellung.

Wie für Kitty-Programm, werden auch bei CAT Zeilenkommentare mit // eingeleitet.

Wir können nun prüfen, ob ein Programm, welches wir mit Hilfe der Technik aus Teil 2 in einen Eventgraphen übersetzt haben, einer formalen Beschreibung der Prozessorarchitektur aus Teil 3 genügt. Dazu gehen wir das gegebene CAT-File Anweisung für Anfweisung der Reihe nach durch. Für Relationsdefinitionen (Def) erweitern wir den gegebenen Eventgraphen entsprechend. Für Bedingungen (Chk) prüfen wir, ob die entsprechende Eigenschaft gilt. D.h. wir prüfen eine Relation auf Kreisfreiheit, Irreflexivität (reduzierbar auf Kreisfreiheit, siehe Teil 3) oder Leerheit. Falls die Bedingung nicht erfüllt ist, verwerfen wir die Ausführung bzw. den Eventgraphen: die Ausführung wird von der Prozessorarchitektur nicht unterstützt, ein Prozessor dieser Architektur legt das Verhalten nicht an den Tag.

Die Hauptaufgabe in diesem Teil des Projektes besteht im Berechnen neuer Relationen und im Prüfen von Kreisfreiheit. Während Kreisfreiheit auf Graphen und Mengenoperationen auf Relationen bekannte Konzept sind, stellen rekursive Relationsdefinitionen die größte Schwierigkeit dar. Um das Vorgehen für rekursive Definitionen zu beschreiben, betrachte eine Definition let rec r = f(r). Hier schreiben wir vereinfachend f für eine Funktion über Relationen; in CAT würden wir statt f(r) eine Relation angeben, zum Beispiel (po; r) & rf*. Unsere rekursive Definition beschreibt diejenige Relation, welche dem Kleinsten Fixpunkt der Gleichung r = f(r) entspricht. Um diesen kleinsten Fixpunkt zu berechnen, führen wir eine Kleene-Iteration¹ durch. Wir beginnen mit der leeren Relation e und berechnen f(e). Nun wiederholen wir die Anwendung von f, d.h. wir berechnen f(f(e)), f(f(f(e))), f(f(f(f(e)))) und so weiter, bis wir zu einem Punkt gelangen an dem f(...) mit f(f(...)) übereinstimmt. Dieser Punkt ist der kleinste Fixpunkt und entspricht der Relation die wir füf r suchen.

¹ Theoretischer Hintergrund, bekannt aus TheoInf1: Relationen über Events Evt sind Mengen der Form Evt×Evt. Da Evt in unserem Fall endlich ist, handelt es sich bei Evt×Evt um einen vollständigen Verband. Ferner ist die Funktion f, die wir zur rekursiven Definition von r verwenden, monoton (unter der Annahme, dass die Differenz von Relation Rel1\Rel2 nur mit konstanten Relationen Rel2 gebildet wird—dies nehmen wir in diesem Projekt an). Somit existiert ein eindeutiger kleinster Fixpunkt, welcher durch Kleene-Iteration gefunden wird.

Sobald die Menge der erlaubten Ausführungen eines Kitty-Programms berechnet ist (Teil 4), kann der Korrektheitstest des Programms ausgeführt werden. Es ist zu beachten, dass wir dazu tatsächlich alle erlaubten Ausführungen benötigen, da die Korrektheitstest über alle Ausführungen quantifizieren (existenziell oder universell). Um den Korrektheitstest auszuwerten, müssen Bedinungen (Cond) auf einzelnen Ausführungen evaluiert werden. Diese Bedinungen sind Boolsche Formeln über Gleichheiten von Registern/Speicherzellen mit Werten. Das Übereinstimmen von Registerinhalten mit bestimmten Werten kann mit der Technik von Teil 2 bestimmt werden. Das Übereinstimmen von Speicherinhalten mit bestimmten Werten ist problematisch, da wir keinen echten Begriff von Speicher und dessen Inhalt haben—das Ziel des Projektes ist es ja gerade von dieser Sicht auf Relationen zu abstrahieren. Um solche Bedingungen dennoch auszuwerten, bedarf es der Coherence Order (co), welche wir in all unseren CAT-Files definieren (genauer: wir inkludieren immer std.cat). Der Speicherinhalt ist dann der Wert, der vom co-latest Write geschrieben wird. Ein Write w ist co-latest, falls (w',w) ∈ co+ für alle anderen Writes w' gilt.

Must Have Die Teilnehmer sollen einen CPU-Simulator entwickeln, der die obigen Teile 1-5 integriert:

• Teil 1Eingabe von Programmen in der Assembler-Sprache Kitty,
• Teil 2Berechnen aller Ausführungen des gegebenen Programms,
• Teil 3Eingabe der zu verwendenden Prozessorarchitektur in der Sprache CAT,
• Teil 4Filtern der berechneten Ausführungen bezüglich der gegebenen Prozessorarchitektur und
• Teil 5Prüfen von Korrektheitseigenschaften.

In Teil 3 ist das Unterstützen der Relationen data und ctrl nicht verpflichtend.

Should Have Zusätzlich wäre es wünschswert (und für die Entwicklung bzw. das Debugging sehr hilfreich), wenn die Ausführungen mitsamt den berechneten Relationen graphisch ausgegeben werden. Die graphische Ausgabe kann z.B. in Form eines .pdf oder .png erfolgen.

Ebenso wünschswert ist eine Implementierung der Relationen data und ctrl.

Could Have Neben den zuvor erwähnten Features sind folgende, weitere Features denkbar, allerdings optional und für den Erfolg des Projekts (sowohl im inhaltlichen als auch im prüfungstechnischem Sinne) irrelevant:

Abgrenzungskriterien Wir weisen ausdrücklich darauf hin, dass dieses Projekt nicht in der technischen Informatik angesiedelt ist. Insbesondere ist es nicht Ziel des Projektes eine spezielle CPU Register-getreu nachzubilden. Im Fokus steht eine allgemeine, formale Beschreibungssprache (CAT), welche das erlaubte Verhalten präzise und prägnant beschreibt.

Für das Projekt interessante Prozessorarchitekturen in Form von CAT-Modellen: Download hier. Einzig das CAT-Modell simple-arm.cat verwendet die Relationen data und ctrl und kann dementsprechend vorerst ignoriert werden.

Ein Sammlung an kurzen, sprungfreien (weder goto noch jumpc) Testprogrammen, sogenannten Litmustest: Download hier.

Für technisches Hintergrundwissen bezüglich CAT kann die Dokumentationvon von diy konsultiert werden. Es ist allerdings zu beachten, dass diy eine komplexere Toolsuite als die unsere darstellt und dementsprechend konvolutiert ist.

Die eingesetzten Techniken können von den Teilnehmern, nach Absprache, frei gewählt werden.

Wir empfehlen den Teilnehmern den Einsatz folgender Techniken:

• Java: gängige Hochsprache
• AntLR: Parsergenerator zum Erstellen eines Parsers für Kitty-Programme und CAT-Modelle

Weitere, ggf. interessante Tools:

• Jetbrains IntelliJ IDEA: exzellente IDE für Java (Lizenzen sind über den Rahmenvertrag der TU Braunschweig erhältlich)
• BigBlueButton: Konferenztool, gehostet durch die TU Braunschweig

Betreut wird das Projekt durch Roland Meyer, Peter Chini, und Sebastian Wolff. Ansprechpartner sind Peter Chini und Sebastian Wolff.