Erste Schritte mit TLA+

Concurrent Design

Bei den ersten Gehversuchen zum Thema Concurrency nahm ich dankbar jede Unterstützung an, die sich anbot: Standard-Library Funktionen zur Thread-Erzeugung, lock_guard, um nicht mehr an die Lock-Freigabe denken zu müssen, std::atomic und dergleichen. Es sind sehr nützliche Werkzeuge für die Implementierung. Und trotzdem war alles wenig hilfreich, wenn es darum ging, mich beim Überprüfen des Designs einer Lösung zu unterstützen. Quellcode scheint nicht dafür gemacht. Die beste mir bekannte Möglichkeit waren Stift, Papier und Nachdenken, Timelines skizzieren, Szenarien (Verhalten) ausdenken und durchspielen und dergleichen. Dazu kommt, dass dieses manuelle Überdenken wenig Sicherheit bietet. Man stelle sich vor, nach Design und Implementierung fallen einem Fehler auf im Betrieb und irgendwann stellt sich heraus, dass das Design fehlerhaft ist. Eine zwingende Anpassung des Designs ist die Folge.

Viele Tests vs. alle Tests

Leider helfen hier auch Tests nicht unbedingt weiter. Während ich möglicherweise prüfen kann, ob ein bestimmtes Verhalten nicht zu einem Deadlock führt, kann ich das Verhalten nicht vollständig und abschliessend prüfen. Race Conditions kann ich mit herkömmlichen Tests nur unzuverlässig oder gar nicht finden. Und falls sporadisch ein Fehler gefunden wird, ist seine Ursache dadurch noch nicht zwingend klar. Ebenso problematisch sieht es aus, wenn ich einen sporadischen Fehler «gelöst» habe und der Test durchläuft: Wurde die Ursache tatsächlich behoben, oder tritt der Fehler lediglich weniger häufig auf?

TLA⁺ und TLC wurde genau dafür geschaffen: Damit kann ein System Design überprüft werden. Natürlich können bei der Implementierung nochmals Fehler gemacht werden. Das Überprüfen auf eine korrekte Implementierung muss anderweitig erfolgen.

In diesem Blog stelle ich TLA⁺ und die dazugehörigen Werkzeuge vor, indem ich zuerst ein naives Design spezifiziere, das eine Race Condition enthält. Danach verbessere ich das Design und prüfe es erneut, um sicherzustellen, dass das Problem nicht mehr auftritt.

Tools

Nebst der Spezifizierungssprache gibt es noch den TLC ModelChecker. Er verwendet eine `.tla` Datei zusammen mit einer Modell Konfiguration und führt die Prüfung des Modells durch. Nur mit dessen Hilfe können Fehlverhalten und Error Trace festgestellt werden.

Diese Werkzeuge sind über die offizielle Seite unter dem Namen Toolbox gebündelt verfügbar: Eine IDE mit TLA⁺ und PlusCal Syntax Support inkl. dem TLC ModellChecker. Die ursprünglichen Video Kurse beziehen sich alle auf diese Toolbox.

Daneben existiert auch eine vscode Extension, die laufend gepflegt wird. Nach der Installation der Extension sind ebenfalls alle benötigten Werkzeuge installiert und in vscode können Spezifikationen geschrieben, PlusCal in TLA⁺ übersetzt und Modelle geprüft werden.

Funktionsweise

Die Überprüfung eines Systemdesigns stützt sich auf folgende drei Punkte:

• Spezifikation: Mit TLA⁺ Syntax (oder PlusCal) wird beschrieben, was das System kann.
• (Invariante) Eigenschaften: Definieren, welche Eigenschaften oder Systemzustände nie zutreffen dürfen.
• ModelChecker: Prüft das System, indem er basierend auf der Spezifikation jedes mögliche Systemverhalten entdeckt und dabei prüft, ob die Invarianten jederzeit erfüllt sind.

Zustände

Ein erstes Beispiel zeigt einen stark vereinfachten Lift, der sich über drei Stockwerke bewegen kann, jeweils ein Stockwerk aufs Mal. Der Lift kann sich auf einem der drei Stockwerke befinden (Unten, Mitte, Oben). Das sind 3 mögliche Zustände des Lifts. Der Lift kann entweder nur nach unten, nur nach oben oder nach unten oder oben fahren, je nachdem in welchem Zustand er sich befindet. Im Modell kann dieser Lift nichts weiter als das, er kann bspw. keine Personen aufnehmen.

Verhalten

Ein Verhalten beschreibt eine mögliche Abfolge von Zuständen basierend auf dem Liftmodell mit den drei möglichen Zuständen. Das Diagramm zeigt alle möglichen Verhalten des Modells mit Initialzustand «Unten»:
Der Begriff «mögliches Verhalten» bezeichnet den Pfad vom Startzustand zu einem anderen Zustand, bspw. «1-2-3» oder «1-2».

Nach dem Zustand 3 sind alle Zustände gestrichelt dargestellt, um zu verdeutlichen, dass es sich dabei um Wiederholungen bestehender Zustände handelt. In diesem einfachen Lift Modell gibt es keine weiteren Variablen wie bspw. Anzahl Personen in der Kabine. Daher handelt es sich ab Zustand 3 nur noch um Wiederholungen, die der ModelChecker auch also solche erkennt und nur die 3 eindeutigen Zustände ausweist (Distinct States = 3).

ModelChecker

Der ModelChecker entdeckt alle möglichen Zustände anhand der Spezifikation. Danach werden alle möglichen Verhalten überprüft. Wird zu irgendeinem Zeitpunkt eine Invariante verletzt, wirft der ModelChecker einen Fehler. Dabei gibt er im Error Trace an, welches Verhalten zum Fehler geführt hat. In diesem ersten Beispiel ist keine Invariante definiert.

Weiterführend

Stuttering, also den Zustand nicht zu wechseln, wird implizit überprüft und ist im Diagramm nicht eingezeichnet. Dies bedeutet, dass der Lift kann auch mehrmals im selben Zustand verharren kann. Es könnte auch auf temporale Eigenschaften geprüft werden. Bspw. ob jedes Verhalten irgendwann einen bestimmten Ausdruck erfüllt. Oder dass nach einem bestimmten Zustand A zwingend irgendwann ein Zustand B erreicht werden muss. Temporale Eigenschaften werden in diesem Blogbeitrag nicht behandelt.

Syntaxvarianten

TLA, TLA⁺ oder TLA⁺2: Gibt es einen Unterschied? Leslie Lamport schuf ab 1990 die TLA Spezifikation, zehn Jahre später folgte der ablösende Standard TLA⁺ und 2006 folgte TLA⁺2. Heute relevant ist ausschliesslich TLA⁺2 unter dem Namen TLA⁺.

Für Einsteiger sorgt die Unterstützung von gleich drei unterschiedlichen Syntaxen für Konfusion: TLA⁺, PlusCal C-Style und PlusCal P-Style. TLA⁺ ist eine Sprache, um ein Systemdesign zu spezifizieren. Die Sprache ist eher mathematisch orientiert. Um Entwicklern von Algorithmen einen einfacheren Zugang zu eröffnen, wurde nebst TLA⁺ ein weiterer Syntax entwickelt: PlusCal. PlusCal Syntax wird innerhalb einer TLA-konformen `.tla` Datei im Kommentar Block am Anfang der Datei gespeichert wird durch den pcal Transpiler in TLA⁺ übersetzt wird. Der dadurch generierte TLA⁺ Code wird unterhalb des PlusCal «Kommentars» eingefügt. Das Resultat ist eine TLA⁺ konforme `.tla` Datei, die anschliessend vom ModelChecker verwendet wird.

Von PlusCal existieren zwei unterschiedliche Syntax Varianten: C-Style und P-Style. C-Style orientiert sich an der Programmiersprache C und verwendet geschweifte Klammern, während P-Style sich an Pascal orientiert und mit `begin .. end` Schlüsselwörtern arbeitet. In diesem Blog wird ausschliesslich PlusCal mit P-Syntax verwendet. In Online Tutorials oder Github Repos kann jedoch beides angetroffen werden, auch TLA⁺ Syntax ist verbreitet.

Beispiele

Einrichten

Für die Beispiele verwende ich vscode mit der Extension «TLA+ (Temporal Logic of Action)» der «TLA+ Foundation». Der `.tla` Dateiname muss mit der ----- MODULE -----  Zeile übereinstimmen: `simplelift.tla` enthält die Zeile ----- MODULE simplelift ----. Mit «F1» «TLA+: Parse Module» erfolgt eine Überprüfung des Codes. Falls erfolgreich, wird der PlusCal Code in TLA⁺ Code übersetzt und im unteren Teil der selben Datei eingefügt. Zudem wird eine `.cfg` Datei angelegt, eine Voraussetzung für den ModelChecker, den ich mit «F1» «TLA+: Check model with TLC» starten kann.

Simpler Lift

Das vorhergehende sehr einfache Beispiel mit der Lift Statemachine kann ich in vscode wie folgt modellieren und «prüfen»:

1. `simplelift.tla` erstellen
2. «F1» «TLA+: Parse Module»
3. «F1» «TLA+: Check model with TLC»
4. Der ModelChecker sollte 3 distinct States finden und erfolgreich enden.

Inhalt von `simplelift.tla` vor der Übersetzung :

---- MODULE simplelift ----

(* --algorithm simplelift

variables 
etage = "unten";

process StateMachine = "SM"
begin
  Action:
    either 
      await etage = "unten";
      etage := "mitte";
    or
      await etage = "mitte";
      etage := "unten";
    or
      await etage = "mitte";
      etage := "oben";
    or
      await etage = "oben";
      etage := "unten";
    end either;
    goto Action;
end process;

end algorithm; *)

====

ModelChecker Output (Auszug):

Model checking completed. No error has been found. [...]
5 states generated, 3 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).
Finished in 629ms at (2024-08-28 15:52:30)

Race Condition

Eine etwas praktischere Situation kann mithilfe einer Getränkestation aufgezeigt werden: Die Station hat zwei Touchscreen Bedienelemente für die Benutzer-Interaktion und unterhalb jedes Panels je einen Auslauf, der die Getränke ausgibt. Wir nennen die Bedieneinheit mit dem zugehörigen Auslauf «Maschine». Beide Maschinen teilen sich einen gemeinsamen Kühlschrank. Der Kühlschrank kann nur von einer Maschine gleichzeitig verwendet werden.  Die Maschine, welche den Kühlschrank nutzt, nennen wir «Controller».

Wenn der Benutzer kaltes Wasser bezieht an der Maschine, fordert diese das Wasser beim Kühlschrank an und ist während dieser Zeit der «Controller». Während dieser Zeit kann die andere Maschine nicht gleichzeitig ebenfalls «Controller» sein und Wasser beziehen. Zur weiteren Vereinfachung wird angenommen, dass wenn eine Maschine ausgeschaltet wird (oder abstürzt), dies dem Kühlschrank mitgeteilt wird. In der Praxis müsste dies der Kühlschrank bspw. über ausbleibende Keepalives selber feststellen. Ein naives Modell sieht dann so aus:

------------------------------- MODULE watersimple -------------------------------

EXTENDS Integers, Sequences, FiniteSets

Machines == 1..2

(* --algorithm water 
variables 
  Fridge = "idle";
  Controller = {};


define   
  TypeInvariant == Fridge \in {"idle", "dispense"}
  OnlyOneController == Cardinality(Controller) <= 1
  ValidController == (Fridge = "dispense") = (Controller # {})
end define

process machine \in Machines 
variables 
  requestFridge = "none";
begin
    UserInput:
    while TRUE do
        either 
            requestFridge := "none";
            if self \in Controller then
                Controller := Controller \ {self};
                Fridge := "idle";
            end if
        or  
            requestFridge := "dispense";
        end either; 

        if self \notin Controller 
            /\ requestFridge = "dispense" 
            /\ Fridge = "idle" then
            TakeControl:
            Fridge := "dispense";
            Controller := Controller \union {self};
        end if;

    end while;
end process;
end algorithm; *)
======

Spezifikations Details

Machines == 1..2

Machines ist ein Set, das alle Ganzahlen von 1 bis 2 enthält. Damit sind Anzahl und Id der Maschinen festgelegt. Bei der Prüfung wird dann nicht nur geprüft mit zwei Maschinen, sondern auch mit einer Maschine.

variables
  Fridge = "idle";
  Controller = {};

Die verwendeten Variablen. Fridge ist entweder «idle» oder «dispense», daran können die Maschinen den Status des Kühlschranks sehen.
Controller ist zu Beginn ein leeres Set. Wenn eine Maschine die Kontrolle übernimmt, wird die Maschinen-Id dem Set hinzugefügt, der Code dazu folgt weiter unten.

define
  TypeInvariant == Fridge \in {"idle", "dispense"}
  OnlyOneController == Cardinality(Controller) <= 1
  ValidController == (Fridge = "dispense") = (Controller # {})
end define;

Diese Operatoren müssen im define Block definiert werden, dann können sie vom modelChecker als Invarianten verwendet werden. TypeInvariant prüft, ob die Variable Fridge den Wert «idle» oder den Wert «dispense» hat und keine ungültigen Werte angenommen hat. OnlyOneController prüft, ob die Anzahl Elemente in Set Controller nicht mehr als 1 beträgt.

Spezifikations Details Prozess

process machine \in Machines
variables 
 requestFridge = "none";

process erstellt in diesem Fall so viele gleichzeitige Prozesse wie Elemente in Machines enthalten sind, bspw. machine[1], machine[2]. requestFridge ist eine Prozessvariable, jeder erstellte Prozess verfügt über seine eigene Instanz von requestFridge. Wenn der Prozess startet, hat sie den Wert «none».

begin
  UserInput:
    while TRUE do
      [ ... ]
    end while;
end process;

begin und end process umschliessen die Anweisungen eines Prozesses. Damit sie zyklisch durchlaufen werden und nicht der Prozess nach einmaligem Durchlaufen stoppt, wird der while Block eingefügt. UserInput ist ein Label. In TLA⁺ werden Labels dazu verwendet, die Gleichzeitigkeit zu definieren. Alle Anweisungen innerhalb eines Labels gelten als atomar ausgeführt.

either 
    requestFridge := "none";
    Controller := Controller \ {self};
    Fridge := "idle";
or  
    requestFridge := "dispense";
end either;

Mit dem either block kann nicht-deterministisches Verhalten beschrieben werden, bspw. Benutzerinterkationen. Das schliesst auch das Verhalten ein, dass immer nur die selbe Option gewählt wird, bspw. wenn jemand einen Kanister mit kaltem Wasser füllen möchte und dazu wiederholt Wasser anfordert. Hier wird beschrieben, dass an der Maschine ein Wasser bezogen werden kann oder nicht. Wird kein Wasser bezogen, wird die Maschine als Controller entfernt, um der Vereinfachung Rechnung zu tragen, die zuvor beschrieben wurde: Der Kühlschrank merkt, wenn er nicht mehr kontrolliert wird.

if self \notin Controller 
  /\ requestFridge = "dispense" 
  /\ Fridge = "idle" then
  TakeControl:
  Fridge := "dispense";
  Controller := Controller \union {self};
end if;

Wenn die Maschine nicht bereits ein Controller ist, eingeschaltet ist und der Kühlschrank als «idle» erkannt wird, übernimmt die Maschine die Kontrolle über den Kühlschrank. Das Übernehmen der Kontrolle erfolgt nach dem Label TakeControl. Die beiden Zuweisungen nach dem Label erfolgen gleichzeitig, aber, wichtig, nicht gleichzeitig mit der vorhergegangenen Prüfung, die noch unter dem Label UserInput erfolgte. Dieser Fehler sollte später durch den ModelChecker erkannt werden. In TLA⁺ sind die Labels immer global. TakeControl und UserInput sind gleichwertige Labels, in TLA⁺ gibt es keine verschachtelten Labels, auch wenn die Einrückung dies suggeriert.

Modell Konfiguration

Die Konfiguration `watersimple.cfg`:

SPECIFICATION Spec

INVARIANT
    TypeInvariant
    OnlyOneController
    ValidController

`INVARIANT` oder `INVARIANTS`: Es werden beide Schreibweisen akzeptiert.

Modell Check

Nachdem ich mit «F1» «TLA⁺: Parse Module» den TLA⁺ Code erzeugt habe, kann ich mit «F1» «TLA+: Check model with TLC» den ModelChecker starten. Der TLC ModellChecker stoppt nach dem ersten gefundenen Problem und meldet: «Invariant OnlyOneController is violated.», was bedeutet, dass Controller mehr als ein Element enthält. Unter Error Trace wird die Abfolge von Schritten aufgezeigt, die zum Fehlverhalten führen. Das Problem ist eine Race Condition: Beide Maschinen erfragen den Zustand des Kühlschranks, während dieser «idle» ist und versuchen dann, die Kontrolle zu übernehmen, was nur dem schnelleren der beiden Maschinen gelingen sollte . Hier führt es dazu, dass beide Maschinen die Kontrolle übernehmen, ein Zustand, den wir explizit als unerwünscht definiert haben. pc steht für program counter und zeigt für jeden laufenden Prozess das aktuelle Label an.

Rückverfolgung des Fehlers

Race Condition lösen mit Zwischenstatus

Der Bug aus dem vorherigen Beispiel kann auf mehrere Arten vermieden werden. Im folgenden Beispiel wird der Kühlschrank um einen Zwischenstatus «reserved» erweitert, in den der Kühlschrank wechseln muss, bevor er kontrolliert werden kann. Eine Maschine kann unter Angabe ihrer ID beim Kühlschrank eine Reservierung platzieren, die nur dann übernommen wird, wenn der Kühlschrank weder reserviert noch in Benutzung ist. Eine Maschine kann nur dann die Kontrolle übernehmen, wenn eine Reservierung besteht, die auf ihre eigene ID lautet. Als ID wird die Prozessnummer verwendet.

------------------------------- MODULE water_reservation -------------------------------

EXTENDS Integers, Sequences, FiniteSets, TLC

Machines == 1..2

(* --algorithm water_lock
variables
  Fridge = "idle";
  FridgeReservedFor = {};
  Controller = {};

define
  TypeInvariant == Fridge \in {"idle", "reserved", "dispense"}
  OnlyOneController == Cardinality(Controller) <= 1
  ValidController == (Fridge = "dispense") = (Controller # {})
  ValidReservation == (Fridge = "reserved") = (FridgeReservedFor # {})
end define;

macro putReservation() begin
    if Fridge = "idle" /\ FridgeReservedFor = {} then 
        Fridge := "reserved";
        FridgeReservedFor := {self};
    end if;
end macro;

process machine \in Machines
variables 
  requestFridge =  "none";
begin
    Mainswitch:
    while TRUE do

        either 
            requestFridge :=  "none";
            if self \in Controller then
                Controller := Controller \ {self};
                Fridge := "idle";
            end if
        or  
            requestFridge := "dispense";
        end either;
        
        CheckConditionReservation:
        if self \notin Controller /\ requestFridge = "dispense" /\ Fridge = "idle" then
            TryReservation:
            putReservation();
        end if;
        
        CheckConditionControl:
        if self \notin Controller 
                /\ requestFridge = "dispense" 
                /\ Fridge = "reserved" 
                /\ self \in FridgeReservedFor then
            TakeControl:
            Fridge := "dispense";
            FridgeReservedFor := {};
            Controller := Controller \union {self};
        end if;

    end while;
end process;
end algorithm; *)
======

Spezifikations Details

variables
  Fridge = "idle";
  ReserveFridgeFor = {};
  Controller = {};

Kühlschrank ist «idle» (nicht kontrolliert, nicht reserviert), «reserved» (reserviert für eine Maschine) oder «dispense» (Kontrolliert durch eine Maschine, liefert Wasser).
Im Falle eine Reservierung ist die ID der Maschine ein Element von Set FridgeReservedFor. Wenn der Kühlschrank kontrolliert wird, steht die Maschinen-ID im Set Controller.

define
  TypeInvariant == Fridge \in {"idle", "reserved", "dispense"}
  OnlyOneController == Cardinality(Controller) <= 1
  ValidController == (Fridge = "dispense") = (Controller # {})
  ValidReservation == (Fridge = "reserved") = (FridgeReservedFor # {})
end define;

Einige Invarianten. Neu werden ValidController und ValidReservation geprüft, die beide gleich funktionieren. Im Falle von ValidController: Wenn Fridge=»controlled» dann darf das Controller Set nicht leer sein und umgekehrt.

macro putReservation() begin
  if Fridge = "idle" /\ FridgeReservedFor = {} then 
    Fridge := "reserved";
    FridgeReservedFor := {self};
  end if;
end macro;

Ein Macro das weiter unten verwendet wird. Der PutReservation Vorgang ist hier als atomar spezifiziert. Erkennbar daran, dass zwischen Zustandsprüfung und Reservation kein neues Label eingeführt wird.

CheckConditionReservation:
if self \notin Controller /\ requestFridge = "dispense" /\ Fridge = "idle" then
    TryReservation:
    putReservation();
end if;

Sind die Vorbedingungen erfüllt, wird versucht, eine Reservation zu platzieren. Diese kann erfolgreich sein oder nicht. Möglicherweise erfolgt durch die andere Maschine eine Reservation zwischen CheckConditionReservation und TryReservation. Dieser Code Teil zeigt ganz gut die Möglichkeit auf, wie durch gezieltes Setzen von Labels Gleichzeitigkeit zugelassen oder gezielt unterbunden werden kann.

CheckConditionControl:
if self \notin Controller 
  /\ requestFridge = "dispense" 
  /\ Fridge = "reserved" 
  /\ self \in FridgeReservedFor then
TakeControl:
    Fridge := "dispense";
    FridgeReservedFor := {};
    Controller := Controller \union {self};
end if;

Auch hier erfolgt das Prüfen der Bedingung nicht zusammen mit dem Übernehmen der Kontrolle als atomarer Block, sondern unter zwei verschiedenen Labels.

Modell Konfiguration

Die `.cfg` Datei definiert mehrere Invarianten, die jederzeit erfüllt sein müssen:

SPECIFICATION Spec
\* Add statements after this line.

INVARIANTS 
    TypeInvariant
    OnlyOneController
    ValidController
    ValidReservation

Modell Check

Der TLC ModelChecker endet ohne einen Fehler gefunden zu haben:

Finished computing initial states: 1 distinct state generated at 2024-09-02 15:40:22.
Model checking completed. No error has been found.
[...]
289 states generated, 115 distinct states found, 0 states left on queue.

Fazit

Das Schreiben von Spezifikationen ist zu Beginn gewöhnungsbedürftig, weil es eine strikte Trennung von Design und Implementierung verlangt. Das zeigte mir auf, dass ich zuvor diese Grenze nicht ganz so scharf wahrnahm, wie sie jetzt von TLA⁺ gefordert wird.

Die grössten Stolpersteine die mir beim Einstieg mit TLA⁺ aufgefallen sind, sollten mit diesem Beitrag aus dem Weg geräumt sein. Im Wesentlich verstand ich den Begriff vom «Verhalten» eines Systems zu Beginn nicht richtig, sondern setzte ihn gleich mit den Transitionen einer Statemachine. Dass drei unterschiedliche Syntaxen existieren und je nach Tutorial einer davon verwendet wird, sorgte bei mir für zusätzliche Verwirrung.

Gerne hätte ich eine echte Situation aus der Praxis verwenden wollen, stellte jedoch fest, dass dies zu einem zu grossen Spezifikationsumfang geführt hätte. Eine simple Race Condition war daher naheliegender. Für solch einfache Fälle braucht es natürlich noch keine formalen Methoden zu Überprüfung. Aber der ModelChecker kann auch Modelle prüfen mit Millionen von Zuständen.

Zwischen den hier verwendeten kleinen Beispielen und einer Spezifikation aus der realen Welt besteht noch eine grosse Lücke. Um wirklich einen Nutzen aus TLA⁺ ziehen zu können, müsste ich mich tiefer damit befassen und sukzessive komplexere Spezifikationen schreiben.

Weiterführende Links

TLA⁺ wird verschiedentlich eingesetzt. Hier sind einige Beispiele aus der Praxis:

• Industrial Use of TLA⁺
• TLA⁺ Industry use- Wikipedia
• How Amazon Web Services Uses Formal Methods
• Formal Methods in Practice: Using TLA⁺ at eSpark Learning – Hillel Wayne – eSpark Engineering Blog

Code Beispiele:

• Github: tlaplus/Examples: Übersichtliche Auflistung von Beispielen mit Angaben zu Schwierigkeit und Syntaxvariante
• Writing Lines Of Code: Blog Serie über TLA⁺ mit Ampelsteuerungs Beispiel

Verschiedene:

• Glossar
• LearnTLA: Umfangreiches Lerninformationen
• Learning TLA⁺ and Model (TLA⁺ Wiki)