Ford+VW: Argo AI - Robotaxi-Startup eingestellt

Leicht schon:

static void *memset1(void *d0, int v0, size_t n) { byte *d, *de; if (n&&d0) { d=d0; de=d+n; do *d= (byte)v0; while (++d < de); } return d0; }

Daß die vorstehende Funktion fehlerfrei ist, ist leicht und schnell feststellbar.

Das Gleichnis hinkt. Eine Anzahl Fehler 0..X können auf natürliche Weise vorhanden sein. Eine Anzahl Beweise >1 normalerweise nicht.

Und den Kurvenradien. Wenn das Ausweichen auf der eingezeichneten Bahn moeglich ist, dann ist die Geschwindigkeit des Autos so niedrig, dass auch eine Vollbremsung vor dem Zebrastrefen noch moeglich ist. Ausserdem waere der Crash mit dem Block auf der Strasse nicht toedlich.

Die Frage die man als erstes beantworten muss, ist wie schnell das Auto maximal sein, das kann man durch ausmessen des Bildes, und z.B hiermit berechnen:

Ansatz: Das Auto soll offenbar 1/8 Kreisbogen (45°) fahren.

Daraus folgt dass der Kurvenradius 1.41 mal so gross ist wie die senkrechte Strecke die das Auto vom beginn des Manoevers bis zum erreichen der 45° braucht. In dem Bild ist diese nichmal 2 Autobreiten, also sagen wir mal 3,6 Meter, das macht einen Kurvenradius von 5.09 Meter und eine maximale Geschwindigkeit von 22.5km/h. Diesen Aufprall sollte man im Auto ueberleben koennen. Der Bremsweg waere dann so ungefaehr um die 3 Meter, also weniger als 2 Autobreiten, soviel Platz ist da auch.

Das hat sich geändert?

SCNR, Alex.

In der Theorie .. in der Realität hat der Begriff "bit rot" Einzug gehalten, üblicherweise wenn die Annahmen von Softwarekomponenten über den Rest des System von der Realität davondriften (Klassiker: fest Verzögerungsschleifen mit NOPs in uralter PC-Software, irgendwann waren dann die CPUs so schnell, das "lange Wartezeit" in Bruchteilen von Sekunden ausgeführt wurde und das zu Problemen führte).

Statischer RAM ist ausserhalb von Sonderanwendungen seit vielen Jahren tot. Kleine Mikrocontroller kann man noch damit ausstatten (u.a. um den Ruhestrom niedrig zu halten) aber als Hauptspeicher aktueller PC (und auch nicht x86 Serversysteme) gibt es seit vielen, vielen Jahren nur noch DRAM.

Die schöne einfache Sicht Fehler/kein Fehler ist schon klar, der Trick ist aber rauszufinden, womit man es zu tun hat. Und der Nachweis von Softwarekorrektheit ist geradezu widerwärtig komplex sobald man sich von Trivialbeispielen entfernt. Die generelle Tendenz, dass die Softwarearchitekturen immer komplexer werden (nicht immer aus gutem Grund) hilft da natürlch auch nicht.

Man liest sich, Alex.

Oh, schöne Falle ;-)

Man liest sich, Alex.

Das ist das Datum deines Postings, dort steht auch dass der Professor das im Jahr 2019 gesagt hat. Ob er inzwischen ueberrascht ist wissen wir nicht. Sicher bedeutet ja "Fahren in San Francisco" nicht alle moeglichen Alltagssituationen, da z.B. Schnee und Eis nicht dabei sind, mit denen man am MIT mindestens 3 Monate im Jahr rechnen muss, aber das hatten wir schon. Die andere Frage ist, was bedeutet "kommen" ? Wenn es zwar mietbare Robotaxis da nicht aber autonome Autos zum kaufen gibt, bedeutet das dann dass das autonome Auto noch nicht da ist ?

Nein, die Kurvenradien sind selbstverständlich symbolisch, und schräg betrachtet, ganz ohne Daten. Andernfalls wäre mindestens ein Raster oder Maßstrich angegeben.

Du verstehst sehr offensichtlich _nicht_ die in den Wissenschaften oftmals verwendeten Annahmen!

Ob das Ausweichen auf der eingezeichneten Bahn möglich ist, ist irrelevant. Es wurde die Annahme getroffen, _daß_ es möglich ist. Ob eine Vollbremsung vor dem Zebrastreifen erfolgreich möglich ist, ist irrelevant. Es wurde die Annahme getroffen, daß eine Vollbremsung _nicht_ erfolgreich ist (Totenkopf A!). Es wurde die Annahme getroffen, daß der Crash mit dem Block unbedingt tödlich ist (Totenkopf B!).

Ohne Annahmen ist die 'Moral Machine' nicht machbar, weil keine wissenschaftliche Arbeit (vernünftig) möglich ist. Der Entscheidungsfall würde gar nicht existieren. Durch Mißachten von Vorgaben wird so ziemlich alles sinnlos.

Komplett irrelevant.

Komplett irrelevant. Du ignorierst die Vorgaben und konstruierst Dir sinnlos etwas zusammen. Die Bildelemente sind symbolisch gezeichnet - nicht real.

Nach 1,7s und 12m Strecke kommt ein Auto zum Stehen (v~0), bei folgenden 'a' und 'v0'. Das MIT hat offenbar deutlich weniger als 12m Haltestrecke angenommen.

a= -8.0 m/s^2 v0= 50 km/h v=[m/s]

t=0.0s s=0.0m vt= 13.888889 vs= 13.888889 t=0.01s s=0.0695m vt= 13.808889 vs= 13.848799 t=0.02s s=0.139m vt= 13.728889 vs= 13.808593 t=0.03s s=0.2085m vt= 13.648889 vs= 13.768269 t=0.04s s=0.278m vt= 13.568889 vs= 13.727827 t=0.05s s=0.3475m vt= 13.488889 vs= 13.687266 t=0.06s s=0.417m vt= 13.408889 vs= 13.646583 t=0.07s s=0.4865m vt= 13.328889 vs= 13.60578 t=0.08s s=0.556m vt= 13.248889 vs= 13.564853 t=0.09s s=0.6255m vt= 13.168889 vs= 13.523803 t=0.1s s=0.695m vt= 13.088889 vs= 13.482627 t=0.11s s=0.7645m vt= 13.008889 vs= 13.441326 t=0.12s s=0.834m vt= 12.928889 vs= 13.399897 t=0.13s s=0.9035m vt= 12.848889 vs= 13.35834 t=0.14s s=0.973m vt= 12.768889 vs= 13.316653 t=0.15s s=1.0425m vt= 12.688889 vs= 13.274835 t=0.16s s=1.112m vt= 12.608889 vs= 13.232885 t=0.17s s=1.1815m vt= 12.528889 vs= 13.190801 t=0.18s s=1.251m vt= 12.448889 vs= 13.148583 t=0.19s s=1.3205m vt= 12.368889 vs= 13.106229 t=0.2s s=1.39m vt= 12.288889 vs= 13.063738 t=0.21s s=1.4595m vt= 12.208889 vs= 13.021107 t=0.22s s=1.529m vt= 12.128889 vs= 12.978337 t=0.23s s=1.5985m vt= 12.048889 vs= 12.935426 t=0.24s s=1.668m vt= 11.968889 vs= 12.892371 t=0.25s s=1.7375m vt= 11.888889 vs= 12.849173 t=0.26s s=1.807m vt= 11.808889 vs= 12.805828 t=0.27s s=1.8765m vt= 11.728889 vs= 12.762337 t=0.28s s=1.946m vt= 11.648889 vs= 12.718696 t=0.29s s=2.0155m vt= 11.568889 vs= 12.674906 t=0.3s s=2.085m vt= 11.488889 vs= 12.630964 t=0.31s s=2.1545m vt= 11.408889 vs= 12.586868 t=0.32s s=2.224m vt= 11.328889 vs= 12.542617 t=0.33s s=2.2935m vt= 11.248889 vs= 12.498209 t=0.34s s=2.363m vt= 11.168889 vs= 12.453644 t=0.35s s=2.4325m vt= 11.088889 vs= 12.408918 t=0.36s s=2.502m vt= 11.008889 vs= 12.36403 t=0.37s s=2.5715m vt= 10.928889 vs= 12.318979 t=0.38s s=2.641m vt= 10.848889 vs= 12.273762 t=0.39s s=2.7105m vt= 10.768889 vs= 12.228378 t=0.4s s=2.78m vt= 10.688889 vs= 12.182826 t=0.41s s=2.8495m vt= 10.608889 vs= 12.137102 t=0.42s s=2.919m vt= 10.528889 vs= 12.091205 t=0.43s s=2.9885m vt= 10.448889 vs= 12.045133 t=0.44s s=3.058m vt= 10.368889 vs= 11.998885 t=0.45s s=3.1275m vt= 10.288889 vs= 11.952457 t=0.46s s=3.197m vt= 10.208889 vs= 11.905849 t=0.47s s=3.2665m vt= 10.128889 vs= 11.859057 t=0.48s s=3.336m vt= 10.048889 vs= 11.81208 t=0.49s s=3.4055m vt= 9.968889 vs= 11.764916 t=0.5s s=3.475m vt= 9.888889 vs= 11.717561 t=0.51s s=3.5445m vt= 9.808889 vs= 11.670015 t=0.52s s=3.614m vt= 9.728889 vs= 11.622273 t=0.53s s=3.6835m vt= 9.648889 vs= 11.574335 t=0.54s s=3.753m vt= 9.568889 vs= 11.526198 t=0.55s s=3.8225m vt= 9.488889 vs= 11.477859 t=0.56s s=3.892m vt= 9.408889 vs= 11.429315 t=0.57s s=3.9615m vt= 9.328889 vs= 11.380564 t=0.58s s=4.031m vt= 9.248889 vs= 11.331604 t=0.59s s=4.1005m vt= 9.168889 vs= 11.282431 t=0.6s s=4.17m vt= 9.088889 vs= 11.233042 t=0.61s s=4.2395m vt= 9.008889 vs= 11.183436 t=0.62s s=4.309m vt= 8.928889 vs= 11.133609 t=0.63s s=4.3785m vt= 8.848889 vs= 11.083557 t=0.64s s=4.448m vt= 8.768889 vs= 11.033279 t=0.65s s=4.5175m vt= 8.688889 vs= 10.98277 t=0.66s s=4.587m vt= 8.608889 vs= 10.932028 t=0.67s s=4.6565m vt= 8.528889 vs= 10.88105 t=0.68s s=4.726m vt= 8.448889 vs= 10.829831 t=0.69s s=4.7955m vt= 8.368889 vs= 10.778369 t=0.7s s=4.865m vt= 8.288889 vs= 10.72666 t=0.71s s=4.9345m vt= 8.208889 vs= 10.674701 t=0.72s s=5.004m vt= 8.128889 vs= 10.622487 t=0.73s s=5.0735m vt= 8.048889 vs= 10.570016 t=0.74s s=5.143m vt= 7.968889 vs= 10.517283 t=0.75s s=5.2125m vt= 7.888889 vs= 10.464284 t=0.76s s=5.282m vt= 7.808889 vs= 10.411015 t=0.77s s=5.3515m vt= 7.728889 vs= 10.357473 t=0.78s s=5.421m vt= 7.648889 vs= 10.303652 t=0.79s s=5.4905m vt= 7.568889 vs= 10.249548 t=0.8s s=5.56m vt= 7.488889 vs= 10.195158 t=0.81s s=5.6295m vt= 7.408889 vs= 10.140475 t=0.82s s=5.699m vt= 7.328889 vs= 10.085497 t=0.83s s=5.7685m vt= 7.248889 vs= 10.030216 t=0.84s s=5.838m vt= 7.168889 vs= 9.9746297 t=0.85s s=5.9075m vt= 7.088889 vs= 9.9187317 t=0.86s s=5.977m vt= 7.008889 vs= 9.8625168 t=0.87s s=6.0465m vt= 6.928889 vs= 9.8059797 t=0.88s s=6.116m vt= 6.848889 vs= 9.7491147 t=0.89s s=6.1855m vt= 6.768889 vs= 9.6919161 t=0.9s s=6.255m vt= 6.688889 vs= 9.6343779 t=0.91s s=6.3245m vt= 6.608889 vs= 9.576494 t=0.92s s=6.394m vt= 6.528889 vs= 9.5182581 t=0.93s s=6.4635m vt= 6.448889 vs= 9.4596637 t=0.94s s=6.533m vt= 6.368889 vs= 9.4007041 t=0.95s s=6.6025m vt= 6.288889 vs= 9.3413724 t=0.96s s=6.672m vt= 6.208889 vs= 9.2816614 t=0.97s s=6.7415m vt= 6.128889 vs= 9.2215638 t=0.98s s=6.811m vt= 6.048889 vs= 9.1610719 t=0.99s s=6.8805m vt= 5.968889 vs= 9.1001779 t=1.0s s=6.95m vt= 5.888889 vs= 9.0388737 t=1.01s s=7.0195m vt= 5.808889 vs= 8.9771509 t=1.02s s=7.089m vt= 5.728889 vs= 8.9150007 t=1.03s s=7.1585m vt= 5.648889 vs= 8.8524142 t=1.04s s=7.228m vt= 5.568889 vs= 8.7893821 t=1.05s s=7.2975m vt= 5.488889 vs= 8.7258947 t=1.06s s=7.367m vt= 5.408889 vs= 8.6619419 t=1.07s s=7.4365m vt= 5.328889 vs= 8.5975135 t=1.08s s=7.506m vt= 5.248889 vs= 8.5325985 t=1.09s s=7.5755m vt= 5.168889 vs= 8.467186 t=1.1s s=7.645m vt= 5.088889 vs= 8.4012641 t=1.11s s=7.7145m vt= 5.008889 vs= 8.3348208 t=1.12s s=7.784m vt= 4.928889 vs= 8.2678436 t=1.13s s=7.8535m vt= 4.848889 vs= 8.2003194 t=1.14s s=7.923m vt= 4.768889 vs= 8.1322345 t=1.15s s=7.9925m vt= 4.688889 vs= 8.0635748 t=1.16s s=8.062m vt= 4.608889 vs= 7.9943254 t=1.17s s=8.1315m vt= 4.528889 vs= 7.9244708 t=1.18s s=8.201m vt= 4.448889 vs= 7.853995 t=1.19s s=8.2705m vt= 4.368889 vs= 7.7828811 t=1.2s s=8.34m vt= 4.288889 vs= 7.7111113 t=1.21s s=8.4095m vt= 4.208889 vs= 7.6386673 t=1.22s s=8.479m vt= 4.128889 vs= 7.5655296 t=1.23s s=8.5485m vt= 4.048889 vs= 7.4916779 t=1.24s s=8.618m vt= 3.968889 vs= 7.4170909 t=1.25s s=8.6875m vt= 3.888889 vs= 7.3417463 t=1.26s s=8.757m vt= 3.808889 vs= 7.2656203 t=1.27s s=8.8265m vt= 3.728889 vs= 7.1886882 t=1.28s s=8.896m vt= 3.648889 vs= 7.1109238 t=1.29s s=8.9655m vt= 3.568889 vs= 7.0322996 t=1.3s s=9.035m vt= 3.488889 vs= 6.9527863 t=1.31s s=9.1045m vt= 3.408889 vs= 6.8723532 t=1.32s s=9.174m vt= 3.328889 vs= 6.7909674 t=1.33s s=9.2435m vt= 3.248889 vs= 6.7085943 t=1.34s s=9.313m vt= 3.168889 vs= 6.6251972 t=1.35s s=9.3825m vt= 3.088889 vs= 6.5407368 t=1.36s s=9.452m vt= 3.008889 vs= 6.4551714 t=1.37s s=9.5215m vt= 2.928889 vs= 6.3684565 t=1.38s s=9.591m vt= 2.848889 vs= 6.2805444 t=1.39s s=9.6605m vt= 2.768889 vs= 6.1913842 t=1.4s s=9.73m vt= 2.688889 vs= 6.1009211 t=1.41s s=9.7995m vt= 2.608889 vs= 6.0090963 t=1.42s s=9.869m vt= 2.528889 vs= 5.9158463 t=1.43s s=9.9385m vt= 2.448889 vs= 5.8211028 t=1.44s s=10.008m vt= 2.368889 vs= 5.7247915 t=1.45s s=10.0775m vt= 2.288889 vs= 5.626832 t=1.46s s=10.147m vt= 2.208889 vs= 5.5271365 t=1.47s s=10.2165m vt= 2.128889 vs= 5.4256095 t=1.48s s=10.286m vt= 2.048889 vs= 5.322146 t=1.49s s=10.3555m vt= 1.968889 vs= 5.2166309 t=1.5s s=10.425m vt= 1.888889 vs= 5.1089371 t=1.51s s=10.4945m vt= 1.808889 vs= 4.9989237 t=1.52s s=10.564m vt= 1.728889 vs= 4.8864341 t=1.53s s=10.6335m vt= 1.648889 vs= 4.7712931 t=1.54s s=10.703m vt= 1.568889 vs= 4.653304 t=1.55s s=10.7725m vt= 1.488889 vs= 4.5322443 t=1.56s s=10.842m vt= 1.408889 vs= 4.4078609 t=1.57s s=10.9115m vt= 1.328889 vs= 4.2798643 t=1.58s s=10.981m vt= 1.248889 vs= 4.1479197 t=1.59s s=11.0505m vt= 1.168889 vs= 4.0116378 t=1.6s s=11.12m vt= 1.088889 vs= 3.8705604 t=1.61s s=11.1895m vt= 1.008889 vs= 3.7241426 t=1.62s s=11.259m vt= 0.928889 vs= 3.5717276 t=1.63s s=11.3285m vt= 0.848889 vs= 3.412512 t=1.64s s=11.398m vt= 0.768889 vs= 3.245495 t=1.65s s=11.4675m vt= 0.688889 vs= 3.0694035 t=1.66s s=11.537m vt= 0.608889 vs= 2.8825748 t=1.67s s=11.6065m vt= 0.528889 vs= 2.6827668 t=1.68s s=11.676m vt= 0.448889 vs= 2.4668275 t=1.69s s=11.7455m vt= 0.368889 vs= 2.2300757 t=1.7s s=11.815m vt= 0.288889 vs= 1.9650032 t=1.71s s=11.8845m vt= 0.208889 vs= 1.6580825 t=1.72s s=11.954m vt= 0.128889 vs= 1.2795459 t=1.73s s=12.0235m vt= 0.048889 vs= 0.72473281 t=1.74s s=12.093m vt= -0.031111 vs= nan t=1.75s s=12.1625m vt= -0.111111 vs= nan t=1.76s s=12.232m vt= -0.191111 vs= nan t=1.77s s=12.3015m vt= -0.271111 vs= nan t=1.78s s=12.371m vt= -0.351111 vs= nan t=1.79s s=12.4405m vt= -0.431111 vs= nan t=1.8s s=12.51m vt= -0.511111 vs= nan

Ich habe für Verzögerungen Interrupts mit globalen In-/Dekrementen benutzt. Auch Hardware-Counter per Makros.

Ich nutzte auch NOPs. Aber mit Berechnung der Zeitdauer einer NOP, abhängig von CLK.

Datentyp byte?

Hmh.

Thomas Prufer

Hallo Helmut,

Du schriebst am Wed, 21 Dec 2022 12:02:53 +0100:

Nein. Sie verhält sich unerwartet, wenn v0 > 255 oder v0 > -256. Hmm, eigentlich tut sie das sogar bei allen Werten von v0 != 0 oder -1. Zumindest, wenn nicht explizit dazugesagt wird, daß der int-Parameter v0 nur als Byte ("(unsigned) char") ausgewertet wird. Ohne diese Information ist die Funktion falsch (fehlerhaft).

Hallo Helmut,

Du schriebst am Tue, 20 Dec 2022 23:10:12 +0100:

Schon, sie wird aber trotzdem auf vielerlei Weise nutzlos oder unbenutzbar.

Klar, mußt Du natürlich nicht. Dann komm' aber nicht mit Deinen "/verträumt/"en Ansichten über die Möglichkeiten zur Umsetzbarkeit solcher Ideen, zumindest nicht solange, bis Du sicher bist, alle Gegenargumente widerlegen zu können. Dazu müßtest Du halt Gödels Theorem bzw. dessen Beweis (!) widerlegen können.

...

Dann lies' halt nach, wasde geschrieben hast. Es ging um obiges.

...

Ja, naja, dann halt die. Und _wonach_ entscheidet die?

Doch, weil _auch_ die ausführende Hardware zu Fehlfunktionen beitragen kann, von den verarbeiteten Daten noch ganz abgesehen.

...

...

Und doch kann es auch da schon zumindest die Anlage zu solchen Problemen geben. Stell' Dir ein System aus mehreren miteinander zusammenarbeitenden Programmen vor, die gegenseitig Daten zur und aus der Verarbeitung austauschen. Kannst Du _sicherstellen_, daß Du jederzeit die jeweils bearbeiteten Befehle ermitteln kannst?

Und solange ist sie halt nutzlos. Wenn sie nie benutzt wird, war der Erstellungsaufwand vergebens.

Bei allen _möglichen_ Kombinationen von allen _möglichen_ Parameterwerten. Das können durchaus "viele" sein...

Korrektur: Ein erwachsener Mensch.

Ein Kind steckt die Brötchentüte u.U. erstmal in den Mund. Du hast jetzt den notwendigen, jahrelangen Lernprozess beim Menschen elegant weggelassen.

Peter

Es gibt auch deutlichere Sprüche:

Man kommt nicht in 1 Monat zu einem Baby, indem man 9 Frauen schwängert.

Peter

Am 20.12.22 um 21:42 schrieb Thomas Prufer:

Das hindert Chuck Schellong doch nicht daran, sich noch mal zum Idioten zu machen.

Hanno

Es gibt schon ein paar formal verifizierte Kernel, Compiler und Betriebssysteme. "Simpel" würde ich die nicht mehr nennen.

Am 19.12.22 um 21:07 schrieb Sieghard Schicktanz:

Formal verifizierte Software existiert.

Hanno

Es ist kein Fehler, einen Datentyp 'byte' zu definieren.

Falls es den in inkludierten Dateien bereits gibt und beide Definitionen nicht genau gleich sind,gibt der Compiler einen Error.

Der C-Standard definiert zudem für das Wort 'byte' nirgendwo irgend etwas. Wenn schon, dann '__byte' oder '_byte' - aber auch das ist nirgendwo belegt.

Das ist eine unzutreffende Behauptung.

Das ist unzutreffend und irrelevant.

Der Typ-cast »*d= (byte)v0;« ist doch in der Funktion klar angegeben.

Du willst einen Fehler herbeireden, den es nicht gibt. Eine Synopsis und Description habe ich nicht angegeben. Der Aufruf der Funktion ist ebenso außerhalb einer Betrachtung.

Es geht nur um den Funktionskörper und den impliziten Prototyp! Das, was ich oben angab. Das schrieb ich sogar bereits im Thread.

Wobei unter Software ein interessanter Absatz steht:

These techniques can be sound, meaning that the verified properties can be logically deduced from the semantics, or unsound, meaning that there is no such guarantee. A sound technique yields a result only once it has covered the entire space of possibilities. An example of an unsound technique is one that covers only a subset of the possibilities, for instance only integers up to a certain number, and give a "good-enough" result.

Letzteres finde ich eher mau... Korrekt ist die Software doch erst dann, wenn sie für ALLE MÖGLICHEN Eingaben (und nicht nur alle erwarteten Eingaben) das jeweils korrekte Ergebnis liefert.

Gerrit