Mit einem ERC „proof-of-concept“-Grant kann Christoph Lenzen, Gruppenleiter am Max-Planck-Institut für Informatik in Saarbrücken die kommerzielle Verwertung seiner „Theorie verlässlicher Hardware“ auf Siliziumchips demonstrieren.
Das Design von Mikroprozessoren ist für einen kurzfristigen Abfall der Versorgungsspannung ausgelegt. Daraus dürfen, vor allem bei kritischen Anwendungen wie Automobilsteuerung, Medizintechnik etc., keine katastrophalen Folgen entstehen.
Hier greift der Ansatz, den Lenzen seit ca. zehn Jahren verfolgt und der seit drei Jahren durch einen ERC Starting Grant gefördert wird: Durch ein Hardware-Design, dass es ermöglicht, Schwierigkeiten, wie Ausfälle oder auch teilweise Beschädigungen innerhalb der integrierten Schaltkreise, so abzufangen, dass das Gesamtsystem weiter funktioniert.
„Stellen Sie sich vor, dass Sie einen Schraubenzieher über Ihren Prozessor ziehen, der danach unter fortlaufendem Beschuss mit Röntgenstrahlung immer noch reibungslos funktionieren soll. Das ist natürlich überspitzt formuliert, aber gar nicht so weit von der Wahrheit entfernt,“ erklärt der Forscher.
Im neuen Projekt liegt der Fokus auf der elektrischen Seite des Chips. Die Forscher um den Saarbrücker Informatiker wollen den Einfluss von Spannungsschwankungen dadurch reduzieren, dass sie die Frequenz des Taktgebers anpassen. Dieses soll durch eine rein digitale Schaltungstechnik ermöglich werden, die schnell genug reagieren kann. Sie ist in der Lage, sowohl sehr steile als auch tiefe Spannungsabfälle abzufangen und die Funktionalität der Schaltung im Betrieb zu gewährleisten.
In seiner Arbeit kam der Forscher zu dem Ergebnis, dass man mit verteilten Algorithmen ein Taktsignal in einem Chip effizienter und zuverlässiger in einem wesentlich größeren Maßstab erzeugen und verteilen kann, als dies mit einem einzigen Taktbaum möglich ist, durch den normalerweise die von einem Quarz erzeugten Taktsignale weitergeleitet werden.
Die Abbildung zeigt einen einfachen fehlertoleranten Taktverteilungsmechanismus. Im Gegensatz zu einem Taktbaum gibt es verschiedene Pfade, auf denen sich das Taktsignal ausbreitet; daher kann das System als Ganzes auch dann noch korrekt arbeiten, wenn einige wenige isolierte Knoten oder Verbindungen ausfallen.
„Eine Besonderheit unserer Herangehensweise ist, dass wir formal die Korrektheit unseres Ansatzes nachweisen. Das heißt, dass wir nicht nur experimentell überprüfen, ob sich das System erwartungsgemäß verhält, sondern mittels mathematischer Beweisverfahren zeigen, dass die korrekte Funktionsweise des Systems zu jeder Zeit gewährleistet ist,“ so Lenzen. Die Entwicklung des erwähnten Computerchips zur praktischen Demonstration der Ergebnisse wird zusammen mit der Gruppe von Prof. Milos Krstic von der Universität Potsdam erfolgen.