1. Foren
  2. Kommentare
  3. Wissenschaft
  4. Alle Kommentare zum Artikel
  5. › Sel4: Fehlerloser Microkernel…

Ach ist das nicht herrlich...

  1. Thema

Neues Thema Ansicht wechseln


  1. Ach ist das nicht herrlich...

    Autor: DerVorhangZuUndAlleFragenOffen 29.07.14 - 18:11

    Dieser Kernel (i.e. ein recht kompliziertes Stück Software) ist absolut fehlerfrei. Wer hat dieses Statement denn abgesondert? Ich glaube nicht das irgendein Entwickler die Chuzpe hat, so etwas ohne Ironie-Tag loszulassen.

    Bleibt die Frage wie die das mit der Fehlerfreiheit beweisen wollen. Schließlich hätten sie dann diverse NP-Probleme im Bereich "Bestimmung der Lösbarkeit von Algorithmen" einfach mal so nebenher erschlagen. Aber wenn die Aussage so stimmt dürfe der nächste Turing-Preis Gewinner wohl feststehen.

    Sorry, aber das Ganze hört sich eher nach Gebrabbel des Marketing an. Die Botschaft hör ich wohl. Allein mir fehlt der Glaube...

    "Entwickeln Sie ein positives Verhältnis zu Daten und freuen sie sich wenn wir mehr wissen!" ~Angela Merkel (12.06.2015)

  2. Re: Ach ist das nicht herrlich...

    Autor: Hello_World 30.07.14 - 00:14

    > Bleibt die Frage wie die das mit der Fehlerfreiheit beweisen wollen.
    So, wie man das eben bei Softwareverifikation macht: mit einem Theorembeweiser, in diesem Fall Isabelle/HOL.

    > Schließlich hätten sie dann diverse NP-Probleme im Bereich "Bestimmung der Lösbarkeit von Algorithmen" einfach mal so nebenher erschlagen.
    Das ist sinnfreies Gebrabbel. Was bitte soll „Lösbarkeit von Algorithmen“ sein? Was soll ein „NP-Problem“ sein? Ich vermute mal, Du meinst die Lösbarkeit eines Problems und NP-schwere Probleme. Natürlich gehst Du mit keiner Silbe darauf ein, welche Probleme das im Kontext von seL4 sein sollen. Zudem lässt deine Formulierung zumindest den Verdacht aufkommen, dass Du nicht einmal verstanden hast, was ein Problem der Komplexitätsklasse NP ausmacht: dass man es lösen kann, wenn auch (vermutlich) nicht effizient.

  3. Re: Ach ist das nicht herrlich...

    Autor: DerVorhangZuUndAlleFragenOffen 30.07.14 - 05:31

    Hello_World schrieb:
    --------------------------------------------------------------------------------
    > > Bleibt die Frage wie die das mit der Fehlerfreiheit beweisen wollen.
    > So, wie man das eben bei Softwareverifikation macht: mit einem
    > Theorembeweiser, in diesem Fall Isabelle/HOL.
    >
    > > Schließlich hätten sie dann diverse NP-Probleme im Bereich "Bestimmung
    > der Lösbarkeit von Algorithmen" einfach mal so nebenher erschlagen.
    > Das ist sinnfreies Gebrabbel. Was bitte soll „Lösbarkeit von
    > Algorithmen“ sein? Was soll ein „NP-Problem“ sein? Ich
    > vermute mal, Du meinst die Lösbarkeit eines Problems und NP-schwere
    > Probleme. Natürlich gehst Du mit keiner Silbe darauf ein, welche Probleme
    > das im Kontext von seL4 sein sollen. Zudem lässt deine Formulierung
    > zumindest den Verdacht aufkommen, dass Du nicht einmal verstanden hast, was
    > ein Problem der Komplexitätsklasse NP ausmacht: dass man es lösen kann,
    > wenn auch (vermutlich) nicht effizient.

    Deine Vermutung ist inkorrekt. Schreibfaulheit dürfte wohl eher der Grund sein. Bei meinem zuvor erwähnten NP-Problem dachte ich konkret die Gruppe der sog. Entscheidungsprobleme. Das Halteproblem dürfte hier wohl das bekannteste sein.

    Egal, das wird jetzt zu müßig das alles aufzudröseln. Wenn du schon automatisierte Theorem-Beweiser ins Spiel bringst, müsstest du zuerst einmal beweisen dass dein automatischer Theorem-Beweiser fehlerfrei ist. Damit beißt sich die Katze in den Schwanz. Es ging mir bei meiner Aussage eigentlich nur darum, dass man eine "absolute" Fehlerfreiheit wohl kaum nachweisen kann. Deshalb auch mein Kommentar mit den Ironie-Tags. Das stellt aber nicht in Frage, dass de-facto (nach bestem Wissen und Gewissen) Fehlerfreiheit nachgewiesen werden kann.

    "Entwickeln Sie ein positives Verhältnis zu Daten und freuen sie sich wenn wir mehr wissen!" ~Angela Merkel (12.06.2015)

  4. Re: Ach ist das nicht herrlich...

    Autor: Hello_World 30.07.14 - 12:19

    DerVorhangZuUndAlleFragenOffen schrieb:
    --------------------------------------------------------------------------------
    > Deine Vermutung ist inkorrekt. Schreibfaulheit dürfte wohl eher der Grund
    > sein. Bei meinem zuvor erwähnten NP-Problem dachte ich konkret die Gruppe
    > der sog. Entscheidungsprobleme. Das Halteproblem dürfte hier wohl das
    > bekannteste sein.
    _Alle_ NP-vollständigen Probleme sind Entscheidungsprobleme, damit erklärst Du also überhaupt nichts. Und welches NP-vollständige Entscheidungsproblem bei Microkerneln wie seL4 auftauchen soll, erklärst Du natürlich auch nicht.

    > Egal, das wird jetzt zu müßig das alles aufzudröseln.
    Ach. Also Du wirfst irgendwelche Schlagworte in den Raum und wenn dann jemand nachfragt, wird es Dir zu müßig? Tipp: nächstes Mal am besten gleich die Klappe halten. Reden ist Silber, Schweigen ist Gold.

    > Wenn du schon
    > automatisierte Theorem-Beweiser ins Spiel bringst, müsstest du zuerst
    > einmal beweisen dass dein automatischer Theorem-Beweiser fehlerfrei ist.
    Nein, bewiesen werden muss nicht die Korrektheit des kompletten Theorembeweisers (der auch Sachen wie Beweistaktiken umfasst), sondern nur, dass die von ihm erzeugten HOL-Beweise für seL4 korrekt sind. Siehe auch de-Bruijn-Kriterium…

    > Damit beißt sich die Katze in den Schwanz.
    Nein, im Prinzip spricht nichts dagegen, die Fehlerfreiheit eines Theorembeweisers zu beweisen. Natürlich würde man die Beweise in der Sprache des Theorembeweisers selbst formulieren, und dann müsste man sie von Hand reviewen. Bei HOL Light arbeitet man an genau so etwas, das ist sicherlich wertvolle Arbeit.

    Das bei seL4 verwendete Isabelle/HOL hat sich in der Praxis aber als wesentlich zuverlässiger als menschliche Reviewer erwiesen. Wenn Du also die Gültigkeit elementarer mathematischer Sätze (z. B. dass Wurzel zwei nicht rational ist) akzeptierst, solltest Du das auch mit dem hier präsentierten Beweis tun.

    > Es ging mir bei meiner Aussage
    > eigentlich nur darum, dass man eine "absolute" Fehlerfreiheit wohl kaum
    > nachweisen kann.
    Kann man und hat man in verschiedenen Fällen getan.

  1. Thema

Neues Thema Ansicht wechseln


Um zu kommentieren, loggen Sie sich bitte ein oder registrieren Sie sich. Sie müssen ausserdem in Ihrem Account-Profil unter Forum einen Nutzernamen vergeben haben. Zum Login

Stellenmarkt
  1. IT-Support / Administrator / Developer für MS-Dynamics (m/w/d)
    Krannich Group GmbH, Stuttgart (Home-Office möglich)
  2. DevOps Engineer Schwerpunkt Microsoft Azure DevOps (m/w/d)
    SEW-EURODRIVE GmbH & Co KG, Bruchsal
  3. Gruppenleitung (m/w/d) IT-Architektur
    ITERGO Informationstechnologie GmbH, Düsseldorf
  4. Referent_in Datenschutz
    Diözesan-Caritasverband für das Erzbistum Köln e.V., Köln

Detailsuche


Golem pur
  • Golem.de ohne Werbung nutzen

Anzeige
Top-Angebote
  1. 32,99€ (Bestpreis!)
  2. 32,99€ (Bestpreis!)
  3. mit bis zu 30% Rabatt
  4. (u. a. MSI Optix G32CQ4DE WQHD/165 Hz für 329€ + 6,99€ Versand und be quiet! Pure Base 600...


Haben wir etwas übersehen?

E-Mail an news@golem.de