Bugs in der STL

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

[AnDasWunderkind]

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

[worstSoftwareErrors]

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?

[fghjrtzedrtsdf]

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.

[knivil]

fghjrtzedrtsdf schrieb:

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.

Warum sollten Prozesse Idiotensicher sein? Wozu benoetigt man dann noch Entwickler? Warum ist fehlerfreie Software so abwegig? Wieso schert sich jeder einen Dreck drum?

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

Ich gebe nichts auf meine Popularitaet, dass du mich achtest oder respektierst.

[MetaPeter]

knivil schrieb:

fghjrtzedrtsdf schrieb:

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.

Warum sollten Prozesse Idiotensicher sein? Wozu benoetigt man dann noch Entwickler? Warum ist fehlerfreie Software so abwegig? Wieso schert sich jeder einen Dreck drum?

Da Menschen Fehler machen und auch machen müssen, ansonsten würde sie sich nie weiter entwickeln, sind auch alle Werke der Menschen mit Fehlern behaftet. Lernen beispielsweise funktioniert nur durch Fehler machen.

Die ganze Evolution beruht auf Fehlern.

Zusätzlich kann das Gehirn des Menschen schlecht objektiv oder im Ganzen denken.

Da wird jetzt aber eine Metadiskussion hier. Also entweder zeigt Knivil nun Einsicht und begreift, warum es keine fehlerfreie Software von Menschenhand geben kann, oder er lässt es halt. Vielleicht findet er wirklich einen Weg 100% fehlerfreie Software zu schreiben und erlangt dann recht schnell Weltrum.

Vielleicht findet es noch heraus wie Gravitation funktioniert und eliminiert oder eliminiert die ganzen Naturkonstanten, damit auch mal die Physik frei von Fehlern wird. Es gibt meines Wissen nämliche keine Naturwissenschaft ohne massig Fehler durch mangelndem Wissen. Es gibt viel mehr Annäherungen und Tricks in den Wissenschaften als wirkliches 100% Wissen. Und das Bild von der Welt, dem Universum oder auch dem Menschen wird sich wohl noch so einige Male komplett wandeln.

Das was wir heute wissen ist ein Witz.

[osdt]

Q: ist es möglich komplexe Software 100% fehlerfrei zu entwickeln?
A: theoretisch ja!

Eine Theorie bleibt eine Theorie bis sie bewiesen werden kann

- osdt

[inkompetent]

fghjrtzedrtsdf schrieb:

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.

Au ja, ich hatte ihm sonst auch eine Kernkompetenz zugeschrieben. Wenn jetzt eine Antwort von ihm kommt, warte ich lieber noch eine andere ab.

[Skym0sh0]

osdt schrieb:

Q: ist es möglich komplexe Software 100% fehlerfrei zu entwickeln?
A: theoretisch ja!

Eine Theorie bleibt eine Theorie bis sie bewiesen werden kann

- osdt

Ich schmeisse einfach mal so theoretische Dinge wie das Hoare-Kalkül und den Satz von Rice in den Raum.

Und daran angeknüpft: Wer meint sein Programm sei fehlerfrei - Beweis oder zählt nicht (auch den Quellcode zeigen reicht nicht! Nur der theoretische Beweis).

[hustbaer]

Skym0sh0 schrieb:

Und daran angeknüpft: Wer meint sein Programm sei fehlerfrei - Beweis oder zählt nicht (auch den Quellcode zeigen reicht nicht! Nur der theoretische Beweis).

Der theoretische Beweis ist, genau so wie ein Programm, ein formales Konstrukt, das fehlerhaft sein kann.
Wenn du sagst "Quellcode zeigen reicht nicht", musst du konsequenterweise auch sagen "Beweis zeigen reicht nicht" - denn dann müsste man erstmal die Korrektheit des Beweises beweisen.
Wo sich dann der Hund in den Schwanz beisst.

[Fehlerkette]

Selbst wenn es möglich wäre 100% fehlerfreien Sourcecode zu schreiben, dann bleiben immer noch fehlerhafte Compiler, Linker, OS, Treiber, Hardware in der Kette stehen. Mal von Designfehlern in der Planung abgesehen.

[kleiner Troll]

@hustbaer
Prinzipiell hast du zwar nicht völlig unrecht, allerdings kann man unter der Annahme das die elementare Logik korrekt ist (und praktisch nimmt man das immer an)durchaus Beweise die gültig sind machen. Aber eben nicht für jedes Programm, die allgemeine Unlösbarkeit des Halteproblems verbietet das. (Zur kleinen Erklärung: Für jedes beliebiges Programm kann man es dann als "korrekt" ansehen wenn es hält. Könnte man also die Korrektheit allgemein zeigen, könnte man auch das Halteproblem lösen. Da das aber nicht geht, kann man im allgemeinen nicht die Korrektheit zeigen)

Damit will ich sagen, das "Richtigkeit eines Programms" eine deutlich andere - viel stärkere - Aussage als "Richtigkeit des Beweises" ist.

Und wenn postuliert das die mathematische Logik korrekt ist, muss man auch Beweise nicht mehr beweisen, deine Rekursionsversuch schlägt also fehl.

[nwp3]

Fehlerkette schrieb:

Selbst wenn es möglich wäre 100% fehlerfreien Sourcecode zu schreiben, dann bleiben immer noch fehlerhafte Compiler, Linker, OS, Treiber, Hardware in der Kette stehen. Mal von Designfehlern in der Planung abgesehen.

Es geht um korrekte Software. Ziel ist es nicht die Korrektheit des Universums zu beweisen. Alles was du nennst ist nicht Teil der Software.

knivil schrieb:

Was fehlt dir, um siche Software zu entwickeln?

Annahme: sicher = korrekt.
Eine Grammatik fehlt. Eine Grammatik, die nur korrekte Programme erzeugen kann. Wenn man die hätte, dann könnte man jedes Programm mehr oder weniger trivial auf Korrektheit prüfen. Die Grammatiken heute finden lexikalische, syntaktische und meinetwegen auch semantische Fehler. Aber sie übersehen logische Fehler.

int getKmInM(int km){
    return km / 1000; //upsi
}

Die Funktion ist Teil eines aus Sicht heutiger Grammatiken völlig korrekten Programms. Aber sie ist falsch. Aufgabe: Finde ein System, was diese Funktion als falsch erkennen würde. Oder ein System, dass die Konstruktion einer solchen Funktion nicht zulässt. Ich kann mir keins vorstellen.

[knivil]

Eine Grammatik fehlt. Eine Grammatik, die nur korrekte Programme erzeugen kann.

Die gibt es fuer ausgewaehlte Domains sicher.

im allgemeinen ... jedes Programm

Es geht aber nicht um jedes Programm.

Traurig, dass man darüber ewig diskutieren muss

Traurig, dass alle einfach nur baschen wollen.

[hustbaer]

@kleiner Troll
Was du schreibst geht leider total an der Realität vorbei.
Du kannst Korrektheitsbeweise leider nicht automatisieren, bzw. keine breit anwendbaren Beweise entwickeln.

Und zwar deswegen nicht, weil "korrekt wenn hält" oder ähnliche einfache, "universelle" Definitionen von Korrektheit totaler Schwachsinn sind.
Üblicherweise schreibt man Programme, um aus einem gegebenem Input einen bestimmten Output zu erzeugen. Und üblicherweise sind die Regeln nach denen das zu passieren hat recht komplex.

Um zu beweisen dass das Programm korrekt ist, musst du beweisen dass es der Vorgabe entspricht. Dass es die definierten Regeln umsetzt.

Dazu brauchst du aber erstmal eine Beschreibung der Regeln. Und zwar eine, die du automatisiert weiterverarbeiten kannst. Oder auf die du zumindest Transformationen anwenden kannst, deren Korrektheit automatisiert überprüfbar ist.
D.h. du musst die Regeln in einer formalen Sprache ausdrücken.

In einer formalen Sprache, wie z.B. ... Lisp.
Und fällt dir was auf? Richtig, jetzt hast du ein Lisp Programm. Und dein toller, semi-universeller Beweis hat bewiesen dass dein XYZ Programm dem Lisp Programm entspricht. Uh yeah bebe, ur a winna!

Und fällt dir noch was auf? Man hätte sich gleich sparen können das XYZ Programm zu schreiben. Schliesslich gibt es Lisp interpreter.

Und fällt dir noch noch was auf? Richtig. Du musst jetzt beweisen dass das Lisp Programm "korrekt" ist - in dem Sinn dass es den Vorgaben entspricht.

[knivil]

korrekt wenn hält

Die Frage nach der Terminierung eines Programms kann fuer viele Programme (unendlich viele) entschieden werden, fuer viele nicht. Das gleiche gilt fuer Fehlerfreiheit bzw. eine Eigenschaft X.

Btw. haben hier recht wenige begriffen, dass es nicht um mein Programm im Speziellen geht. Es geht um die Existenz fehlerfreier Software im allgemeinen. Diese Fehlerfreiheit muss auch nicht zwingend formal bewiesen werden, da beispielsweise der Konstruktionsprozess das eben garantiert.

Desweiteren verstehe ich nicht, warum fehlerfrei Software dermassen auf Widerstand stoesst. Uebertragen beisielsweise auf fehlerfreie Bruecken: Eigentlich duerfte die Golden-Gate-Bridge oder jene ueber unseren kleinen Bach nicht benutzt werden, da damit gerechnet werden muss, dass sie einstuertzt. Als Argumentation wird dann immer die Tacoma Narrows Bridges angefuehrt.

Du musst jetzt beweisen dass das Lisp Programm "korrekt" ist

In Pearls of Functional Algorithm Design wird ebenfalls von einem Programm ausgegangen, dessen Korrektheit leicht bewiesen werden kann aber ineffizient ist. Durch aequivalente Umformungen wird es in ein effizientes Programm transformiert. Du siehst, es ist nicht zwingend problematisch ein weiteres Programm als Ausgangspunkt zu haben.