KittyCAT SEP2020

KittyCAT SEP2020

News

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.

Überblick

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

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;
Dekker's Mutex in C-ähnlichem Pseudocode.

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.

Kitty-Assembler-Programme
CPU-Simulator Teil 1

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 ')'
Syntax von Kitty-Programmen.

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:

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;
Dekker's Mutex in Kitty.

Von Kitty zu Eventgraphen
CPU-Simulator Teil 2

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 }
Ein Kitty-Beispielprogramm.

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:

Program Order des obigen Kitty-Programms.

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.

Erweiterung des obigen Beispiels um die Reads From Relation.

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;
                               }
Ein Kitty-Programm mit abhängigen Writes.

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.)

Eventgraph mit abhängigem Write.

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:

Reads From Relation bei abhängigen Writes.

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;              }
}
Ein Kitty-Programm mit Sprunganweisung.

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:

Eventgraph für obiges Kitty-Programm mit Sprunganweisung.

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:

Eventgraphen mit höchstens vier Events.

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;
}   
Ein Kitty-Programm mit swap.

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:

Eventgraphen für obiges Kitty-Programm mit swap.

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.

Relation rmw für swap.

CAT als formale Beschreibung von Prozessorarchitekturen
CPU-Simulator Teil 3

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
Syntax von CAT.

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

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

Name Kurzbeschreibung Formale Beschreibung
_ All Events Menge aller Events: _Evt.
0 ("Ziffer Null") Empty Set Leere Menge von Events: 0 ≔ ∅.
R Reads Menge aller Read-Events: R ≔ { eEvt | ∃ xv. e = rd(x,v) }.
W Writes Menge aller Write-Events: W ≔ { eEvt | ∃ xv. e = wr(x,v) }.
M Memory Events Menge aller Events, die auf den Speicher zugreifen: MRW.
IW Initial Writes Menge der initialen Write-Events, IWW, die aus der Kitty-Initialisierung @init stammen.
A Atomics Menge aller Read und Write Events, AM, die von Kitty's swap Commands stammen.
MFENCE Fence Events Events, die von Kitty's mfence Commands stammen.
SFENCE Fence Events Events, die von Kitty's sfence Commands stammen.
LFENCE Fence Events Events, die von Kitty's lfence Commands stammen.
Eventmengen von CAT, wobei Evt die Menge aller Events im betrachteten Eventgraphen ist.

CAT definiert folgende Basisrelationen, wobei Evt wie oben:

Name Kurzbeschreibung Formale Beschreibung
id Identity Setzt jedes Event zu sich selbst in Beziehung: id ≔ { (e,e) | eEvt }.
po Program Order Kontrollfluss der Programmausführung in jedem Prozess, poEvt×Evt; siehe Teil 2.
rf Reads From Schreib-Lese-Beziehung zwischen Writes und Reads, rfW×R, wobei (e1,e2) ∈ rf bedeutet, dass e2 den von e1 geschriebenen Wert liest, d.h. e1 = wr(x,v) und e2 = rd(x,v) für ein x,v; siehe Teil 2.
loc Same Location Setzt Events, die auf die selbe Adresse zugreifen, in Beziehung: loc ≔ { (e1,e2) ∈ Evt | locof(e1) = locof(e2) }, wobei locof(rd(x,v))=x und locof(wr(x,v))=x.
ext External Setzt Events von verschiedenen Prozessen in Beziehung, extEvt×Evt, sodass (e1,e2) ∈ ext genau dann wenn die Events e1 und e2 von unterschiedlichen Prozessen stammen.
int Internal Setzt Events innerhalb eines einzigen Prozesses in Beziehung, intEvt×Evt, sodass (e1,e2) ∈ ext genau dann wenn die Events e1 und e2 von ein und demselben Prozess stammen.
rmw Read/Write Exclusive Pairs Setzt Read- und Write-Events in Beziehung, die zusammen eine erfolgreiche atomare Read-Modify-Write Instruktion modellieren, rmwR×W. In den aus Kitty-Programmen resultierenden Eventgraphen sind dies die Events, welche von swap generiert werden, siehe Teil 2
data Data Dependency Setzt Read- und Write-Events in Beziehung, wobei der vom Write geschriebene Wert vom Read abhängt, datapoR×W. In den aus Kitty-Programmen resultierenden Eventgraphen sind dies die Events, welche von %r := [x] und [x] := %r Commands generiert werden, die in Sequenzen der Form %r := [x]; stmt*; [x] := %r; auftauchen, wobei stmt* keine erneute Zuweisung an %r enthält
ctrl Control Dependency Setzt Read-Events, die jumpc-Commands beeinflussen, in Relation zu den Events des gewählten Branches, ctrlpoR×Evt. Also (rd(x,v),e) ∈ ctrl genau dann wenn rd(x,v) aus Command %r := [x] stammt und e aus einem Command stammt, welches nach einem jumpc %r label im jeweiligen Branch ausgeführt wurde. Der jeweilige Branch ist hier der Teil nach Label label falls v != $0 und andernfalls der Teil nach jumpc.
Basisrelationen von CAT, wobei Evt die Menge aller Events im betrachteten Eventgraphen ist.

Die Relationen data und ctrl sind optional, siehe Aufgabenstellung.

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

Identifizieren erlaubter Ausführungen
CPU-Simulator Teil 4

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-Iteration1 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.

1 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.

Korrektheitstest
CPU-Simulator Teil 5

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.

Aufgabenstellung

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

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:

(Syntactic Sugar)
Es ist denkbar, die Sprach aus Teil 1 um if und while Konstrukte zu erweitern, um den Code besser lesbar zu machen.
(Compiler)
Ein Compiler, der ein Programm in C-ähnlichem Pseudocode in ein Kitty-Programm übersetzt. Dieser Compiler würde, zum Beispiel, die momentan händische Transformation von Dekker's Mutex aus dem einführenden Kapitel in die Kitty-Version aus Teil 1 übernehmen. Dieses Arbeitspaket ist eine Übermenge von "Syntactic Sugar".
(GUI)
Eine GUI, die es dem User leichter macht zu einem Programm (i) alle Ausführungen anzusehen, (ii) welche Ausführungen der Architektur nicht genügen und warum und (iii) die Korrektheitstest und ihre Begründung zugänglich macht.
(Vergleich)
Ein Vergleich mit diy oder ähnlichen Tools aus der Literatur, welche wir in diesem Projekt nachbilden.

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.

Resourcen

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.

Technischer Spielrahmen

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

Wir empfehlen den Teilnehmern den Einsatz folgender Techniken:

Weitere, ggf. interessante Tools:


Wir möchten den Teilnehmer des Projekts so viel Freiheit in der Durchführung geben wie möglich. Allerdings müssen die durch das ISF festgelegten formalen Rahmenbedingungen des SEPs eingehalten werden. Insbesondere betrifft dies (i) den Umfang der Dokumente, (ii) Abgabeart und Abgabetermine, (iii) das Benutzen von SVN und Redmine und (iv) das Einbringen eines jeden Teilnehmers an jeder Abgabeentität.

Betreuer

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