Bugs in der STL

Bashar

Mal als Anmerkung: Fehlerfreiheit beliebiger Software zu beweisen ist a priori etwas anderes und vor allem schwerer als fehlerfreie Software zu konstruieren.

dot

Bashar schrieb:

Mal als Anmerkung: Fehlerfreiheit beliebiger Software zu beweisen ist a priori etwas anderes und vor allem schwerer als fehlerfreie Software zu konstruieren.

Das mag sein, aber auch für das konkrete Beispiel sollte das bereits unmöglich sein!? In keinem Fall ist allerdings wäre "Anforderungen, System, Hardware, Software und Use cases offenlegen" ein Beweis...

knivil

Das mag sein, aber auch für das konkrete Beispiel sollte das bereits unmöglich sein!?

Ich frage mich, warum viele auf "Unmoeglichkeit" bestehen. Unter welchen Voraussetzungen ist es denn nicht unmoeglich? Es wirkt auch leicht widerspruechlich, eine Art formalen Beweis zu fordern, aber auf der anderen Seiten so unkonkret zu sein.

In keinem Fall ist allerdings wäre "Anforderungen, System, Hardware, Software und Use cases offenlegen" ein Beweis...

Nein, es versetzt dich aber in die Lage, dich selbst zu ueberzeugen. Es ist die Grundvoraussetzung der Ueberpruefbarkeit. Da das nicht gegeben ist, kannst du mir glauben oder eben nicht. Ich kann erahnen, fuer was du dich entscheidest.

Shade Of Mine

knivil schrieb:

Ich habe hier ein nicht-triviales Programm zu Beleuchtungssteuerung. Das ist zustandsbehaftet. Laeuft auf auf einem Mikrokontroller, kommuniziert ueber RS232 nach aussen. Ein formaler Beweis der Korrektheit ist vielleicht moeglich, aber nicht praktikabel oder gar notwendig. Es wurde mit spezifischen Anforderung in endlicher Zeit erstellt. Es kann mit mehr als den spezifizierten Ausnahmesituationen umgehen. Es kann leider nicht damit umgehen, wenn das Geraet hart mit einem Hammer getroffen wird. Ist es deswegen fehlerhaft?

Ach, da kann ich unmengen an Gegenbeispiele bringen.

Folgendes zB:
Mein Vater hatte mal mit einer Software zu tun die irgendwas tat und dann bei einer Änderung der Daten automatisch ein Backup auf Floppy Disc erstellt hat. Hat einwandfrei funktioniert. Die Daten wurden auf die Festplatte und auf die Floppy geschrieben. Nur manchmal 2-3 im Jahr war ein Datenstand auf der Floppy Schrott. Das war egal weil es bei der nächsten Änderung eh wieder in den Korrekten Zustand gesetzt wurde. Es ist deshalb auch ein gutes Jahrzehnt nicht aufgefallen. Ein Jahrzehnt(!) während es in etlichen Betrieben täglich verwendet wurde.

Im Endeffekt hat mein Vater den Fehler dann gefunden, eine Funktion war nicht reentrant safe. Trivial. Aber hat sich halt nur ganz ganz selten gezeigt der Fehler. Auch wenn es Niemanden aufgefallen ist.

Ich habe einige solche Anekdoten - ist nur langweilig das hier zu zitieren. Software kann Jahrzehnte lang "fehlerfrei" laufen bis man einen Fehler entdeckt.

Shade Of Mine

knivil schrieb:

Es wirkt auch leicht widerspruechlich, eine Art formalen Beweis zu fordern, aber auf der anderen Seiten so unkonkret zu sein.

Nope. Nichts unkonkret. Bleib bitte sachlich.

Die Forderung ist nach einem Formalen Beweis der Fehlerfreiheit. Den du nicht erbringen kannst. Keiner kann das. Ergo ist Fehlerfreie Software unmöglich. Denn wenn sie möglich wäre, müsstest du es ja beweisen können, oder?

Zu Beweisen dass Software Bugs haben kann, ist dagegen trivial. Fast jede Software hat einen eigenen Bugtracker wo die gefundenen Bugs gelistet sind.

knivil

Anekdoten habe ich auch genug, die meisten fallen unter NDA. Ich will auch gar nicht abstreiten, dass Software fehlerhaft sein kann. Es ist sogar sehr wahrscheinlich, dass Software fehlerhaft ist. Akzeptabel ist fuer mich trotzdem nicht. Das allgemeine Mantra/Sing-Sang geht mir auf den Keks. Deswegen ist es mir eigentlich auch nicht wichtig zu beweisen, ob ich oder andere fehlerfreie Software produzieren oder nicht.

Wichtig ist fuer mich, was mich in die Lage versetzt, fehlerfreie Software zu produzieren. Was sind die Umstaende und wie aufwendig es ist, sie herzustellen.

Ergo ist Fehlerfreie Software unmöglich. Denn wenn sie möglich wäre, müsstest du es ja beweisen können, oder?

Nein, Software hat Fehler oder eben nicht. Unabhaengig, ob ich einen Beweis anstrebe oder eben nicht. Normalerweise aber: Da die Fehlerfreiheit nachtraeglich schwer zu beweisen ist, soll sie durch den Konstruktionsprozess gesichert werden. Aber nur weil in jedem Konstruktionsschritt fehler auftreten koennen, heisst das noch lange nicht, dass wirklich Fehler aufgetreten sind.

Jockelx

Ich finde die Diskussion zwar sowieso nicht so toll, aber die Argumentation

Shade Of Mine schrieb:

Die Forderung ist nach einem Formalen Beweis der Fehlerfreiheit. Den du nicht erbringen kannst. Keiner kann das. Ergo ist Fehlerfreie Software unmöglich. Denn wenn sie möglich wäre, müsstest du es ja beweisen können, oder?

kann ich nicht nachvollziehen.

Die Riemannsche Vermutung ist (noch) unbewiesen. Keiner kann sie beweisen.
Sie ist also falsch, denn wäre sie richtig, müsste man sie ja beweisen können.
Oder wie?

junta

knivil schrieb:

Das allgemeine Mantra/Sing-Sang geht mir auf den Keks.

Dein Gelabere langweilt mich auch schon eine Ewigkeit. DU bist also mit Abstand klüger als alle anderen, denn die haben nachweislich verbuggte Software produziert, und sei es nur die Annahme, dass ein Programm nicht länger als 99 Jahre läuft...

Wenn man mal von kleinen Programmen auf einem Microcontroller absieht, verwendet man idr. auch Libraries von anderen, deren fehlerfreiheit man nicht garantieren kann.

Und wie festgestellt, nützt dir ein fehlerfreier Quelltext nichts, wenn der Compiler ein fehlerhaftes Compilat erstellt.

Traurig, dass man darüber ewig diskutieren muss

Programme mit <10 Codezeilen scheinen fehlerfrei umsetzbar zu sein. Und Programme mit 11 Zeilen? Ich behaupte mal, bis 1000 Zeilen ist fehlerfreiheit gut machbar, wenn mans drauf anlegt.

Wenn man dann das Programm ganz klar in Module mit <1k Zeilen unterteilt und diese zusammensetzt sollte das Endergebnis auch wieder fehlerfrei sein, wenn es nicht allzu viele Module sind.

Also hätte man mit etwas Sorgfalt 100k Zeilen grosse Projekte erzeugt.

Von den praxisnahen Alles-ist-Buggy-Verfechtern:

junta schrieb:

Und wie festgestellt, nützt dir ein fehlerfreier Quelltext nichts, wenn der Compiler ein fehlerhaftes Compilat erstellt.

Wie oft ist dir das schon mal passiert?

DocShoe

dgtasersyd schrieb:

junta schrieb:

Und wie festgestellt, nützt dir ein fehlerfreier Quelltext nichts, wenn der Compiler ein fehlerhaftes Compilat erstellt.

Wie oft ist dir das schon mal passiert?

Mit dem Codegear RAD Studio 2007: Mindestens drei mal.

Bashar

dgtasersyd schrieb:

Programme mit <10 Codezeilen scheinen fehlerfrei umsetzbar zu sein. Und Programme mit 11 Zeilen? Ich behaupte mal, bis 1000 Zeilen ist fehlerfreiheit gut machbar, wenn mans drauf anlegt.

Was hat das mit der Anzahl der Codezeilen zu tun? Ich kann ein Programm schreiben, das 10000mal "Hallo, Welt!" ausgibt (ja, ohne Schleife), das ist dann fehlerfrei. Andererseits kann es sein, dass ein Algorithmus in 10 Zeilen falsch ist, ohne dass es einer merkt. (Beispiel binäre Suche)

Wenn man dann das Programm ganz klar in Module mit <1k Zeilen unterteilt und diese zusammensetzt sollte das Endergebnis auch wieder fehlerfrei sein, wenn es nicht allzu viele Module sind.

Vielleicht setzt man sie ja falsch zusammen.

Was hat Fehlerfreiheit mit Quellcode zu tun? Ich finde nicht viel.

Jodocus

Für mich bedeutet "fehlerfreies Programm" im folgenden, dass ein reales Programm jederzeit und ausschließlich die vom Programmierer beabsichtigten Aufgaben erfüllt.

Ein fehlerfreies Programm, welches auf einer echten Maschine läuft, kann nicht existieren (bzw. statistisch liegt die Wahrscheinlichkeit wohl in den Größenordnungen, wie die, dass alle deine Moleküle im Körper thermisch nach oben sausen und du kurz von alleine abhebst).

Selbst wenn bei der Herstellung der Hardware und der Compiler kein Fehler gemacht wurde, alle benutzten Libraries fehlerfrei sind bzw. man keine benutzt, kann das Programm sich nicht gegen alle Einflüsse wappnen, z.B. beliebiges menschliches Versagen, Stromausfall, ...

Selbst wenn man das alles ausschließen könnte, kommt man eben an physikalische Limits, z.B. thermische Fluktuationen in den Transistoren, Bitflip durch kosmische Strahlung, Ionisation durch radioaktive Zerfälle, ... (http://en.wikipedia.org/wiki/Soft_error)

Wie kann man überhaupt sicher sein, alle möglichen externen Fehlerquellen zu kennen?

Niemand, auch nicht knivil, kann garantieren, dass ein Programm fehlerfrei ist. Das ist einfach nicht wahr.

Wenn man das Programm hingegen so lange abstrahiert, bis nichts mehr von der physikalischen Umwelt und nur noch der theoretische Algorithmus auf einem isolierten Maschinenmodell übrig ist, so kommt man in Gefilde, wo man Fehlerfreiheit durchaus beweisen könnte.
Die Fehleranfälligkeit des Programms korrelliert natürlich stark mit der "Komplexität" des Algorithmus (jetzt nicht die aus der Komplexitätstheorie, wie man die hier definiert ist so 'ne Sache, auf jeden Fall muss sie auch einen Zusammenhang mit der tatsächlichen quantitativen Größe (Codelänge) des Algorithmus haben, man kann's ja z.B. mit der Shannon-Entropie definieren, dann wäre ein Tausend-Zeiler Hello-World trotz seiner Größe wertlos, aber Sachen wie Multithreading wären noch gar nicht betrachtet etc. pp.). Es ist also auch schon in der Theorie mutig (um nicht zu sagen töricht), man habe schon subjektiv "sehr komplexe" Programme/Algorithmen geschrieben, die fehlerfrei sind, obwohl man das nicht oder nur empirisch bewiesen hat (wobei empirische, reale Beweise bei theoretischen Algorithmen sowieso nicht ziehen, siehe soft error und auch ohne die können z.T. nach Jahren keine Aussagen getroffen werden, siehe Bsp. von Shade of Mine).

Die oben definierte Komplexität des Beweises einer solchen Fehlerfreiheit eines Algorithmus wird aber wohl oder übel stark mit der Komplexität des Algorithmus selber korrellieren (wenn nicht sogar bei weitem übertreffen), sodass ein solcher Beweis für einen subjektiv großen Algorithmus sowieso total utopisch ist. Wenn wir uns nicht mal aufgrund seiner Komplexität sicher sein können, dass der Algorithmus stimmt, muss man sich um einen Beweis garkeine Sorgen machen, den bekommt man dann eh nicht hin.

Vermutlich versteht knivil einfach was weniger strenges unter Fehlerfreiheit. Egal, auch wenn nicht, die strengste Definition mag echte Fehlerfreiheit vielleicht nicht verbieten, aber gewiss doch so unwahrscheinlich machen, dass auch knivil sie mit seinem Menschenhirn nicht hinbekommt.

hustbaer

@Jodocus
Was haben menschliches Versagen, Strahlung etc. mit dem Programm zu tun?
Also wieso sollte das Programm "nicht fehlerfrei" sein, nur weil Menschen Fehler machen oder die Hardware versagen kann?

Also diese Definition halte ich für ganz groben Unsinn.

Ebenso gehören Fehler im Compiler bzw. den Libraries eben zum Compiler oder den Libraries. Wenn man Binaries betrachtet, dann sind diese Fehler da natürlich mit drinnen, d.h. wenn man von Binaries spricht dann sind diese bei solcherart geerbten Fehlern nicht "fehlerfrei".
Wenn die Fehler in Libraries/Compilern bekannt sind, und man für "fehlerfrei" fordert dass Workarounds für alle bekannten Fehler in anderen Teilen gemacht werden, dann kann man auch sagen das Programm ist fehlerhaft wenn solche Workarounds fehlen.

Aber davon abgesehen... ?

Bzw. wenn eine CPU Serie wiedermal nen Bug hat. Wieso sollte ein ansonsten fehlerfreies Programm dann auf einmal nichtmehr fehlerfreie sein? Das macht doch keinen Sinn. Das ganze System ist in dem Fall nicht fehlerfrei, klar, aber das Programm ist ja nicht das ganze System.

Jodocus

Was haben menschliches Versagen, Strahlung etc. mit dem Programm zu tun?

Die wenigsten Programme überprüfen, ob sich Bits auf dem RAM zwischendurch geändert haben könnten.
Es ist doch die Aufgabe des Algorithmus darauf zu achten, dass seine Eingabe (aus dem RAM) immer gültig ist, bevor er mit ihr arbeitet. Jeder würde erwarten, dass single-threaded Code wie

int array[] = { 1, 2, 3, 4 };
const int index = 3; // man kann const auch weglassen, die Garantie von Seiten von C++ hält immer noch
some_algorithm(index); // wegen call-by-value
return array[index]; // z.B. in einem EAX-register

einmal kompiliert absolute fail-safe ist. Von der Logik der Programmebene her ist eine Speicherzugriffsverletzung beim Arrayzugriff unmöglich, aber ein spontaner Bitflip auf dem RAM in index kann den Zugriff ungültig machen.
Richtiger wäre vielleicht:

int array[] = { 1, 2, 3, 4 };
const int index = 3; // jetzt ist index vielleicht in einem CPU-Register sicher vor "kosmischen Flips", falls der Compiler daraus entsprechenden Code macht
some_algorithm(index); // jetzt wird der Inhalt des Registers auf dem Stack gerettet, dort könnte er aber unerwartet modifiziert werden
asm {
   lea ebx, index ; jetzt wird der Wert zurückgeholt und auf Plausibilität geprüft
   cmp [ebx], 3
   jz correct_code
   call fehler
   mov eax, -1
   ret
   correct_code:
   lea edx, array
   add edx, [ebx]
   mov eax, edx ; array[3] zurückgeben
   ret
}

Klar wäre es in fast allen Fällen total paranoid, auf sowas zu achten, es könnte sogar Performance kosten. Nur weil C++ irgendwas garantiert (hier, dass index nicht geändert wird), muss es eben z.B. nicht korrekt sein. Jeder nimmt das in Kauf, weil es statistisch vernachlässigbar ist (außer in extremen Fällen, wo man tatsächlich Überprüfungen dieser Art macht).

Klar, wenn du annimmst, dass dein Programm fehlerfrei ist, solange seine Umgebung (Runtime, die Maschine, ...) fehlerfrei ist, dann ist das Programm eben aber auch nur unter Vorbehalt echt fehlerfrei. Vielleicht ist der gleiche Code auf einer CPU ohne Baufehler tatsächlich vollständig korrekt.

Bzw. wenn eine CPU Serie wiedermal nen Bug hat. Wieso sollte ein ansonsten fehlerfreies Programm dann auf einmal nichtmehr fehlerfreie sein?

Das hast du dir selbst beantwortet, ersetzte Compiler durch CPU:

Wenn die Fehler in Libraries/Compilern bekannt sind, und man für "fehlerfrei" fordert dass Workarounds für alle bekannten Fehler in anderen Teilen gemacht werden, dann kann man auch sagen das Programm ist fehlerhaft wenn solche Workarounds fehlen.

Wenn Code auf einer neuen CPU mit Baufehler funktionieren soll und die Workarounds nicht eingebaut sind (sofern sie in so einem Fall überhaupt existieren), dann ist der Code einfach falsch.

Jede Naturwissenschaft gibt zu, dass Theorien nicht exakt oder fehlerfrei sind. Exakt und fehlerfrei ist höchstens Mathematik (vorausgesetzt es gibt keine Widersprüche in den Axiomen). Warum sollte praktische Informatik da eine Ausnahme sein? Man kann bei gewissen Algorithmen beweisen, dass sie fehlerfrei sind, weil man so viel von der Wirklichkeit wegabstrahiert. Tut man das nicht, werden solche Beweise aberwitzig und keiner würde sie machen. Und die Algorithmen wären unbrauchbar, unperformant, nicht wartbar, ...

hustbaer

@Jodocus
Sorry, aber Nein!

Wovon du sprichst ist ein EDV System. Also Hardware + Software + evtl. noch Support-Hardware (Netzwerk, USV, ...). Wenn du menschliches Versagen noch mit reinnehmen willst ist es sogar mehr als ein EDV System. Keine Ahnung wie man dazu dann noch sagen soll. Nur "System" wäre ein möglicher Begriff, aber das ist dann schon wieder sehr unspezifisch.

Egal. Zurück zum EDV System.

Ein solches besteht aus vielen Komponenten. Und "das Programm" ist eine dieser Komponenten. Wenn eine der Komponenten fehlerhaft ist, dann kann es sein (muss aber nicht sein), dass das System als Ganzes fehlerhaft ist.
Dass das System als Ganzes fehlerhaft ist bedeutet aber im Umkehrschluss nicht, dass jede Komponente fehlerhaft ist.

Konkret: wenn die CPU hin ist, ist deswegen noch lange nicht das Programm fehlerhaft.
Genau so wenig ist das Programm fehlerhaft weil mal durch kosmische Strahlung oder Quantenunsicherheit irgendwo ein Bit im RAM umgefallen ist.

Wenn beim Auto das Differential kaputt ist, ist deswegen ja auch nicht der Motor fehlerhaft.

----

Ich gebe zu dass der Begriff "Programm" nicht genau umrissen ist, und man durchaus verschiedene Dinge meinen kann wenn man "Programm" sagt/schreibt.

Manchmal meine ich nur den Source-Code (exklusive Source von Thirdparty Libraries), manchmal den gesamten Source-Code, manchmal das fertige Binary (nur die .EXE) und manchmal das Binary + sämtliche Dependencies (inklusive OS).

Aber Hardware ist da niemals inbegriffen.

----

Und was du z.T. Bits im RAM umfallen und Plausibilitätstests schreibst ist auch reiner Quark. Plausibilitätstests in Software sind nicht paranoid, sie sind total sinnfrei und plem.
Wenn es wichtig genug ist dass nix passiert, dann muss ECC RAM her. Dafür wurde ECC schliesslich erfunden.

Der Versuch das in Software nachzubilden ist total sinnfrei. Damit das funktionieren kann, müsste man alles in Assembler schreiben. Inklusive eigenem OS. Jedes PUSH/POP auf den bzw. vom Stack müsste verifiziert werden. Bei jedem Kontext-Wechsel oder Interrupt müssten Prüfsummen über die Registerwerte gerechnet werden uswusf. Die MMU kannst du auch vergessen, da auch die MMU Werte aus dem RAM lädt und diese nicht "prüft" bevor sie sie verwendet. Kurz gesagt: es ist von vorn herein zum Scheitern verurteilt.

Und selbst wenn man es irgendwie hinbekommen würde alle Fälle abgedeckt zu haben, macht es immer noch keinen Sinn. Weil ECC einfach viel viel sicherer ist. Und auch viel günstiger.

----

tl;dr: Es macht nicht immer Sinn alles holistisch zu betrachten.

@knivil: Setze dich doch einfach mal mit dem Militär und der NASA zusammen, die wären froh über fehlerfreie Software. Das kostet nämlich unheimlich viel Geld die Fehler zu minimieren, komplett ausgeschlossen hat sie bis heute noch kein Mensch auf der Welt.

Das Internet ist ja voll mit Beispielen von sehr üblen Software-Fehlern. Hier mal ein Link. Ich glaube nicht, dass da unfähige Leute am Werk waren oder das immer die QA schlecht war.

http://www.sundoginteractive.com/sunblog/posts/top-ten-most-infamous-software-bugs-of-all-time/

knivil

Kenne ich. Beisielsweise koennte

# 10 - Mars Climate Orbiter Crashes (1998)
A sub contractor who designed the navigation system on the orbiter used imperial units of measurement instead of the metric system that was specified by NASA.

vermieden werden, indem Werte an Einheiten durch einen geeigneten Datentyp gekoppelt werden, was eigentlich trivial ist. Gleiches gilt fuer die Ariane 5. Aber genau wie alle anderen Beispiele verstehe ich nicht, was das jetzt beweisen soll? Genauso die Behauptung, dass alles furchtbar teuer ist, etc. ... Wo her kommen diese Behauptungen? Was ist mit all den Softwareentwicklungsprozessen, die eben genau das vermeiden sollen? Und warum packen alle gleich immer Large-Scale-super-duper-komplex aus, was ist mit einfacher Steuerungssoftware oder Kalibrierungsprogrammen. Die wenigsten werden wohl Software fuer den extraterrestrischen Einsatz schreiben.

Ich verstehe auch nicht, was der ganze Hohn und Spott soll. Fehlerfreiheit ist nicht Gott gegeben und faellt auch nicht vom Himmel. Hat nichts mit Wunderkind oder Arroganz zu tun. Innerhalb des Prozesses koennen Fehler gemacht aber korrigiert werden. Wo ist das Problem?

knivil schrieb:

Innerhalb des Prozesses koennen Fehler gemacht aber korrigiert werden. Wo ist das Problem?

Dass es scheinbar keinem außer Dir gelingt. Es gibt keinen Prozess der so idiotensicher ist, dass jeder Fehler vermieden werden kann.

Ich dachte bisher Du hättest Erfahrung und Ahnung. Das hätte sich mit diesem Thread erledigt.