Posts by hybrid

    Danke für den Upload. Da die Abmeldefrist für den Termin der heute war bereits am 26. endete und ich zu dem Zeitpunkt noch keine Unterlagen hatte, hatte ich mich abgemeldet, will ja niemandem den Platz wegnehmen bei begrenzter Platzzahl. Aber mal schauen, ob es im Herbst einen Prüfungstermin gibt.

    Schließe mich an, konnte mich zur VO im WS12 leider nicht anmelden (will das Fach seit mehreren Semestern machen, war dann immer Abgesagt, hatte es in dem Semester dann wohl schlicht übersehen), daher kein Zugang zu TUWEL.
    Für den Fall, dass man die Prüfung auch ohne Anmeldung machen kann wär's auch nett wenn mir jemand die Unterlagen zulassen kommen könnte.

    Hatte mich gerade wegen dieses Problems gewundert, danke.
    Noch was dazu - da es ja nur eine UF H dann gibt kommt die auch ned in den functional constraints FC vor oder? Nur in der flat.

    Finde leider dazu nix - was sagt der type bei zb s_int_variable eigentlich aus? In Beispielen steht immer wieder 3 als type. Ist das selbst zu definieren, also alle s_int_variable(<Wert>,3) stehen für dieselbe Variable, id=3 quasi, und die Werte werden versucht? Oder ist der type irgendwas vordefiniertes bzw was?

    Mir ist da einiges noch nicht ganz klar.


    Wir lassen das ganze in zwei Schleifen ablaufen, für die Fuzz-Variablen (size und die Strings) und für die Fuzz-Strings (die tatsächlichen Werte von size und den Strings?) oder?


    Da wir ja bei jeder neuen Serververbindung einen neuen Bug bekommen, sollen wir Verbindung erstellen, Server mit allen möglichen gefuzzten Nachrichten bombadieren und hoffen einen Bug auszulösen, Verbindung trennen? Oder wie in dem Beispiel im O'Reilly-Buch pro Fuzz-String Verbindung herstellen und trennen, was uns jedes mal einen neuen, anderen Bug generiert?
    Aufgrund des Verhaltens des Servers bezüglich Bug-Generierung würd ich eher ersteres tippen oder?


    Da wir ja die Schleife pro Fuzz-Variable und String durchlaufen lassen, müssen wir im Endeffekt für jeden Transport-Header-Typ und Service-Header-Typ je die zwei Schleifen machen?
    zb fürs STATUS_REQUEST fuzzen wir Size und die String-Payload (auch die leer sein kann beim STATUS_REQUEST?) Also 2 Variablen, soviele Werte für den Fuzz-String wie er machen will.


    Dann fürs STATUS dasselbe, und für die anderen, und für die verschiedenen Services sowieso nochmal mehr?
    Oder wie kriegen wie all die verschiedenen Transport- und Service-Typen in insgesamt 2 Schleifen, wenn die Schleife auf die Variablen gehen und diese Typen-Felder aber "fix"/nicht gefuzzt werden?
    In der inneren Schleife wo der Fuzz-String gefuzzt wird jeweils ein Spike für jeden Typ basteln und abschicken? Also in der inneren Schleife 10 Spikes oder so an den Server schicken? Sicher nicht des schönste, aber könnts so gehn?


    Die Doku zu Spike ist ja echt miserabel, ohne die bereits hier gelinkte hätt ich noch weniger Ahnung als ich hab, was ohnehin nicht viel ist...


    Weiters - man baut ja den Spike immer erst in der Fuzz-String-Schleife zusammen, also definiert auch die Variablen erst dort? Kommt mir komisch vor, da die Fuzz-Variablen ja in der äußeren Schleife abgefragt werden? Richte mich hierbei wieder nach dem O'Reilly Beispiel zb.


    Kommt eigentlich vom Server jemals irgendwas zurück? Oder kann man sich Abfragen diesbezüglich eigentlich sparen?


    Kann man eigentlich die Spike-Größe begrenzen auf die maximal 4096 (über Block-Größen?)? Wenns größer ist wirds der Server ja nicht annehmen oder? Oder ist das auch ein "gültiger" zu fuzzender Fehlerfall?

    edit:nvm (war kurz nicht per ssh erreichbar, library problem besteht nach wie vor)


    edit: Ich habs jetzt mal ganz auf nummer sicher und dreckig gemacht, hab -L/path_to_library und -I/path_to_includes für die library und die spike.h gemacht, damit funzt #include<spike.h> endlich, aber sollt die nicht eigentlich in der library enthalten sein? Oder wird für jede library die header-file in /usr/include gelegt?
    Dazu hab ich die library noch in /usr/local/lib und /usr/lib gehaut und LD_LIBRARY_PATH gesetzt. Krieg jetzt zwar auch bei einfachem spike_connect_tcp Aufruf wie kuetsch oben nen segfault, aber zumindest kann man mal damit arbeiten.
    Jetzt hoff ich mal das funzt mit den Libraries aufn bandit bis ich soweit bin das Ding abzugeben...


    Ist das einbinden dynamischer Libraries immer so ne Qual oder is Spike da einfach schlecht oder is da irgendein Fehler drinnen?


    Hab die LVA-Leitung angeschrieben, spike war nicht installiert am bandit, ist es jetzt, aber die Meldung wegen openssl/ripemd.h krieg ich immer noch.

    Habs jetzt mal am bandit getestet, dasselbe. Verwende die Makefile die sie uns gegeben haben, habs mit #include<spike.h> (was ja stimmen sollt oder, wegen der dynamic library?) und #include"spike.h" versucht, in der default shell und in der bash - meldet immer, dass er spike.h nicht kennt, außerdem ebensowenig die openssl/ripemd.h die in der common.h includet wird.

    Hab wie schon kuetsch Schwierigkeiten die Library überhaupt zu verwenden, könnte vielleicht jemand kurz was dazu sagen?
    Hab einen soft link /usr/lib/libspike.so auf die libspike.so im SPIKElib gesetzt (hatte die libspike.so auch schon selbst reinkopiert in /usr/lib, nich gefunzt), hab des -lspike wie gehabt im Makefile, wenn ich dann aber #include<spike.h> in der fuzzer.c hab meint er immer, dass er spike.h nicht findet. Hab auch das Spike-lib Verzeichnis zum LD_LIBRARY_PATh hinzugefügt.


    Wurde btw beim Suchen der Spike-Installation aufn bandit noch nicht fündig, wo sind die da überhaupt?

    Funzt das kompilieren aufn Server bei euch? Versuch grad mal ne so gut wie leere fuzzer.c (wollt am Wochenende dran arbeiten, hatte mir aber die Angabe und die Files etc. davor nicht gesichert, und dann war die Seite die ganze Zeit off ... -.-) zu kompilieren, mit deren Makefile und common.h und krieg ne Meldung, dass openssl/ripemd.h nicht gefunden wird?

    Bin noch am Arbeiten vom Extrahieren, grundsätzliche Frage ob das so passt hoffentlich bisher:
    Ich seh mir im Root Directory Table an welche Files zum Root directory gehören (nur DAT-Files übrigens, keine MP3, JPG, sonstwas, kommt mir komisch vor, passt so?) und mit dem offsets die nötigen Informationen (Dateiname, Extension, Start im Cluster und Dateigröße). Mit den Werten spring ich in die Data Region (Offsetberechnung wie bei den vorhergehenden Posts oben) und hol mir den bytecode von Start der Datei bis Start+Größe, das lass ich als neue File ausgeben, Dateiname+Extension die ich vorher ausgelesen hab.
    Oder gibts da einfachere Möglichkeiten zum Extrahieren? Ne Weile nicht mehr wirklich viel mit C gearbeitet, gibts da irgendeine extract()-Function oder sowas in irgendeiner Library? Oder gehts nur per Hand quasi?


    Wenn dann die Dateien "extrahiert" sind halt irgendwie weiter damit umgehn, schau ich mir dann an wenn's soweit ist.


    Bzgl Teil 1 - daran hatte ich gedacht, quasi das einzige, das mir eingefallen wäre dazu (Anzahl der Integer = Anzahl der Jobs, Größe der Integer = Dauer der Jobs etc.) dachte aber dass es nicht in Ordnung wäre die Anzahl der Prozessoren auf 2 zu beschränken. Hatte schon dran gedacht, ob es zumindest möglich wäre sie >= 2 und even() zu setzen, dann würd ich halt jeweils die Hälfte der Prozessoren einer Partition gegenüber setzen.

    da es im tiss 2 prüfungstermine am 29 juni gibt, und zwar 4.(letzter) termin WS11 und 1. Termin SS12, vermute ich ganz stark dass du im juni trotzdem keine aufs SS12 ausgerichtete und eventuell 'bessere' prüfung bekommen wirst


    Najo, bei der Prüfung am 3.2. wars genauso und die vom SS11 meinten zb sie hatten den AP-Determinismus nie der bei uns im WS 11 kam. Außerdem, vergleich die letzten drei Prüfungen, vom WS11, mit denen davor, speziell zb Teil 4. Nur Bisimulation die letzen drei Male, davor nicht.

    Tjo... bis zum Juni-Termin dann und hoffen, dass die dann wohl aufs SS12 ausgerichtete Prüfung besser ist?


    Teil 4 war wieder mal Bisimulation.
    Teil 3 musste man assert e zur Sprache aus den Folien hinzufügen aber mit allem Drum und Dran, wp, wlp, sp, partial und total correctness Hoare Regeln, Syntax, Semantik, das ganze noch beweisen und ohne bestehende Statements zu nutzen.
    Teil 2 war einerseits wieder ein simplified Tseitin beweisen wie schon paar mal, und ein einfaches Sparse Method Beispiel, aber mit Erklärung zu jedem Schritt, wie was wieso warum, Hintergründe, Zusammenhänge hinter der ganzen Methode.
    Teil 1 musst ich kräftig schlucken als ich "NP-Hardness sah". War dann doch "nur" eine Reduktion um die NP-Hardness zu beweisen, aber konnte mit den beiden Programmen nichts anfangen.
    War einerseits das laut Angabe bekanntermaßen NP-Harte Partition (Ist es möglich ein Set aus n Integern so in zwei Sets einzuteilen, dass die Summen der beiden Sets gleich groß sind?), andererseits das zu reduzierende Multiprocessor Scheduling oder so (Ist es möglich bei x Jobs mit Laufzeit y und z Prozessorkernen a) das Scheduling so hinzukriegen, dass die einem Prozessor zugeteilten Jobs direkt nacheinander abgearbeitet werden und b) ist es möglich, dass die minimale Abarbeitungszeit für die Jobs Summe der Dauer aller Jobs durch Anzahl der Prozessoren ist).
    Bahnhof wie man da reduzieren soll.


    Bis Juni und hoffentlich danach nicht nochmal im Wintersemester...

    Hoi


    Meine die Prüfung hier, im Forum ist bei den diversen 6.5. Beiträgen wohl von der anderen Prüfung, alter Modus?, die Rede weil sich die Lösung nach nem ganz anderen Beispiel anhört.


    Find die Kripke Structure ziemlich interessant und knifflig, hab jetzt ne überraschend simple Lösung die hoffentlich stimmt?


    K = (S,T,L)
    S = {s0, s1, s2, s3, s4}
    L = {(s0,leer), (s1,q), (s2, p), (s3, leer), (s4, leer)}
    T = {(s0,s1), (s0, s2), (s1, s3), (s3, s3), (s3, s2), (s2, s4), (s4, s4), (s4, s1)}


    Dachte mir

    is zu sehen anhand s0 -> s1 -> s3 (-> s3) -> s2. Die zweite Formel ist dasselbe, nur mit q und p vertauscht und die Kripke halt dementsprechend anders zu traversieren. Die "darf nicht sein" Bedingung tritt eh nie ein, da auf keinem Pfad global nicht-p oder nicht-q kommt.


    Kommt mir sehr einfach vor und ned sicher ob es stimmt, aber meine Überlegungen waren:


    AG (q -> (-p ... heißt ja, dass wenn in einem Knoten q vorkommt, darf kein p vorkommen. Dann ...
    *und* AX (-p *und* A (-q U p) ..... in keinem Nachbarn eines q-Knotens darf ein p vorkommen und es kommt auf allen Pfaden solang kein q bis ein p kommt. Das ist imo erfüllt, in s3 ist kein p und kein q, dort kann geschleift werden bis dann nach s2 gesprungen wird zum p. Da ja nur p und q nicht vorkommen dürfen kann man das ja schon in einem Knoten machen oder?

    Nur zur Sicherheit - die For-Schleife soll maximal n-mal laufen oder? Also nicht auf n+1 etc. erhöhen, weil was würde dann passieren? Also nach n Durchläufen, Sprung in die Endlosschleife, Semi-Decidability. "Erlaubt" ist die Konstruktion weil ja Exists-Halting ohnehin irgendwie entscheiden muss ob es hält oder nicht, kann man diese Entscheidung genausogut nach Special-Halting abgeben?
    Im Endeffekt machst du eine Reduktion und nimmst diese als Semi-Decision Procedure her, sowas gabs ja bisher nicht bei den Prüfungen/Aufgaben oder? Nur dass ich es hoffentlich richtig verstehe.