Mars-robottens to millioner linjer C-kode renset for fejl inden landing

C kode, er kendt for at give problemer, på grund af manglende typetjek, mangel på tjek ved brug af dynamisk hukommelse, manglende analyserbarhed på grund af brugen af pointere mv. Hvorfor bruge et sprog som C, og ikke f.eks. ADA?

De skriver at koden er "gennemtjekket". Betyder det, at det reelt ikke er brugt C, men at der er defineret en C variant, som er muligt at lave automatisk tjek-software til, og eventuelt kompatibelt med C, så det kan oversættes med almindelige C eller C++ compilere, og samtidigt automatisk tjekkes grundigt igennem med test softwaren?

Da sonden Mars Climate Orbiter i 1999 gik tabt på vej i kredsløb om Mars, skyldtes det en sammenblanding af metriske (SI) og amerikanske måleenheder.

Det er jo en typisk typetjek fejl. Hvis der blev brugt et sprog, som håndterede SI enheder, og amerikanske enheder, så kunne problemet nemt undgås. Enheder, og enhedstjek, burde være en del af ethvert programmeringssprog.

Jeg ved at der er en måde at lave C programmer på som bil industrien bruger.
Den bruger ret mange tests.

... ellers ville jeg nok bruge SPARK(1), der er et subset af Ada til sådan noget som Mars Curiosity roveren.
Den er meget god til at fange fejl, hvis man også er god til at specificere præcis, hvad softwaren skal gøre.

Man kan hente en Free (GPL licens) af en Ada 2012 compiler og et SPARK 2012 tool set (også GPL licens) gratis på (2), så det er nemt at komme i gang uden omkostninger.

SPARK er meget begrænset og ikke altid det rigtige programmeringsprog til opgaven, f.eks til alm. PC programmer, hvor det er meget mindre katastrofalt med fejl.

Her benytter jeg mig af D programmeringssproget (i version 2).

D har ikke en WM a la Javas JVM. Compileren laver maskinkode.

D har understøttelse for actor baseret concurrency a ala Erlang programmeringssproget. Actor baseret concurrency er: Send en besked. Det er type sikkert.

Dertil også en garbage collector for klasser, som man også kan slå helt fra i en kritisk sektion af sin kode, hvor en garbage collection, der sætter alle tråde i dvale, er meget ubelejligt.
Man skal naturligvis huske at slå den til igen, og det gør man i en scope(exit) { blok } i en funktion/metode, som for normal afvikling af programmet eller exceptions - altid vil blive kørt.

Der er ikke en preprocessor i D, da man under oversættelse har adgang til et stort subset af D programmeringssproget.

Templates/Generics: Nogen siger at Ds templates er nemmere at bruge end C++s tilsvarende, og at man også kan mere end C++ templates.

Kig på (3) - brug dmd compileren (4), og Phobos standard biblioteket (5) - det gør du automatisk hvis du bruger reference implementationen af Ds compiler, dmd.

ADA, SPARK Links:
=================

(1):
http://en.wikipedia.org/wiki/SPARK_%28programming_language%29
http://www.altran-praxis.com/spark.aspx

(2):
http://libre.adacore.com/download/configurations

D programmeringssprog links:
============================

(3):
http://dlang.org/
http://dlang.org/comparison.html
Language reference, Begynder her: http://dlang.org/lex.html

(4):
Hent kun version 2 af compileren, [b]ikke[/b] version 1:
http://dlang.org/download.html

(5):
http://dlang.org/phobos/index.html

Det kunne være interessant at høre om hvilke andre tests de udfører.

Den med de forskellige enheder burde kunne være fanget med simple integrationstests eller ved at simulere landingen.

Det hedder MISRA C, http://www.sgvsarc.com/Overview/misra_c_static_checking.htm

Det er ikke så meget andre tests, som det mere er en bestemt måde at designe og implementere softwaren på.
- f.eks. ingen allokering af hukommelse run-time - det fjerner en god bunke fejlmuligheder.
- void pointers (void*) er også forbudt.

Wikipedia har nogle links: http://en.wikipedia.org/wiki/MISRA_C#External_links
- ikke mindst nævnes adressen på det oficielle website: http://www.misra.org.uk/

I reglen bruger man kun en delmængde af C, da fuld C er stort set umulig at gennemanalysere statisk. Blandt andet er malloc() og relaterede funktioner bandlyst.

Nogen gange kører man checket på den genererede maskinkode i stedet for kildeteksten, for så behøver man ikke stole på oversætteren.

Ada bliver skam brugt til kritiske missioner -- til den højeste klasse af kritiske missioner tillader ESA assembler, C og Ada, og for C's vedkommende uden malloc() m.m. C++ er bandlyst til kritiske funktioner.

Når man ikke bruger sprog og compilere designet til verificerbarhed, skyldes det nok en ekstrem grad af konservatisme -- man laver ikke noget om, med mindre der er meget stærke grunde til det.

Når man ikke bruger sprog og compilere designet til verificerbarhed, skyldes det nok en ekstrem grad af konservatisme -- man laver ikke noget om, med mindre der er meget stærke grunde til det.

Vil ikke være naturligt, at NASA fra start definerer et højpålideligt sprog, som de bruger ved alle missioner?

Fejl, som f.eks. rod i amerikanske/europædiske enheder, vil kunne undgås, ved at sproget indeholder tjek for enheder. Ofte, er praktisk, at selv kunne definere enheder, såsom ms/tick, tap/rotation, ms/tap, taps/tapwheel. Der findes ingen fysisk størrelse uden enhed og angivet fysisk nøjagtighed.

For at det fungerer skal man vel hive typerne helt ud i protokollaget, da fejlen var at enheden der blev sendt (pund/sekund) og modtaget/fortolket (newton/sekund) var forskellig.

For at det fungerer skal man vel hive typerne helt ud i protokollaget, da fejlen var at enheden der blev sendt (pund/sekund) og modtaget/fortolket (newton/sekund) var forskellig.

Det rigtige vil være, at bruge samme sprog hele vejen igennem.

Der findes mange compilere til C/C++, og mange bibliotekskomponenter. Det kan være en årsag til, at vælge C/C++. Et sprog kan evt. være tæt op til C/C++, så det er nemt, at rette koden til, og evt. kan det fungere med C, men give warnings, hvis ikke koden rettes. Problemer som enhedstjek, automatisk analyse af tilstrækkelig beregningsnøjagtighed, analyse af max. forsinkelse i softwaren og svartid, vil være eksempler på tjeks, som vil være naturligt, at kunne udføre på sproget. I styringssammenhæng, kan måske også være en fordel, at udvikle tools, og evt. implementere det som funktion i sproget, som kan tage problemer skrevet matematisk med differentialligninger, og omsætte dem til differensligninger og kode, og kunne analyseres, således worst-case præcision på værdier og tid, kan udregnes, og garenteres umuligt kan overskrides. Ved fysiske størrelser, er enhed og præcision vigtige tjeks. Ofte sker fejl, hvis der ikke er styr på enheder, timing nøjagtighed, beregningsnøjagtighed, målenøjagtighed på input, og afrundingsnøjagtigheder, f.eks. på grund af begrænsning af bit. En statisk analyse af nøjagtighed, er sammen med timinganalyse og enhedstjek, meget vigtigt for sprog der styrer noget fysisk.

En grund kunne jo også være, at de gode programmører bruger C, medens der måske er mindre kritisk masse heraf på ADA.

Og nej - et programmeringssprog kan ikke kompenserer for talentløshed og kun i noget omfang for sjusk.

Der fiindes altså adskillige gode programmører der bruger Ada.

Programmeringssproget, kan ikke kompensere for talentløshed, men mange fejltyper kan opdages, f.eks. problemet med enheder, som tidligere har været et NASA problem. Skal du kompensere for talentløshed, så er den bedste måde, at lave enentydige specifikationer, og sætte flere hold - mindst to - til at lave præcist samme software, og så tjekke, at det virker ens. Eventuelt, kan flere programmørers software, tjekkes ved flertalsafstemning i softwaren, således et program der fejler, kobles ud.

Naturligvis fordyres omkostningerne en smule - men der opnås større sikkerhed, fordi såvel specifikationens enentydighed tjekkes, og programmørenes arbejde tjekkes.

Kombineret med et programmeringssprog, der tjekker det, som kan tjekkes automatisk, så er muligt at opnå stort set fejlfrit software. Men naturligvis, kan altid være fejl udenfor softwaren, f.eks. i modeller.

I nogle tilfælde, kan et godt programmeringssprog, kompensere for tallentløshed, ved at ganske enkelt indeholde gode konstruktioner, og være lavet af dygtige personer. C, og C++, er eksempler på sprog, hvor du nemt kan falde i, fordi det ikke er lavet af dygtige dataloger. Som eksempel, bruges ofte 0 terminerede strenge, der har en O(n) svartid, og det kan medføre, at softwaren bliver langsom. Et godt programmeringssprog, har længdefelt først i strengen, således det ikke tager tid, at finde strengens længde. Et supergodt sprog, har mulighed for længdefelt af flere typer, fra byte til longint, eller endnu flere bytes, afhængigt af hvor stor strengen max. er defineret til. Hvis du implementere gode konstruktioner i sproget, og sikrer at sproget er lavet så programmøren motiveres til, at bruge disse, så undgår du ofte dårlige implementeringer, såsom bobbelsort, dårlige søgemetoder mv. Det er vigtigt, at et sprog motiverer til, at bruge det korrekt.

Mange tests, f.eks. timinganalyse, har til formål, at tjekke programmørenes talent. Hvis en rutine ikke svarer hurtigt nok, eller har for stor store O funktion, så opdages, at programmøren mangler noget kunnen, og at vedkommende måske har brug for hjælp, til at løse de tungere algorithmer.

@Erlo
Ingen anfægter at der findes gode ADA-programmører. Der blev blot postuleret at der er flere gode C-programmører, da sproget er mere udbredt. Der er ganske givet også flere elendige C-programmører.

@Jens Madsen
De få case-studies jeg har læst om NASA/ESA etc. giver mig ikke anledning til at tro at det er effektivitet/optimalitet af algoritmer der giver problemer. ESA's Ariane raket gik ned pga. en signed/unsigned fejl, så variablen der holdt en acceleration, blev negativ og derfor vendte styringen raketten om (meget forsimplet og frit fra hukommelsen).
Fejlen med pund/sekund vs newton/sekund har heller ikke noget med algoritmer at gøre, men vel nærmere noget med specifikationer og snitflader.

MISRA-C kan verificeres i højere grad end fuld ANSI-C med statisk analyse, men typeløse enhedsfejl f.eks. kan vel kun fanges i dynamisk/runtime-test.

Jeg kunne også godt tænke mig at høre lidt mere teknisk om den statiske analyse. Jeg bruger selv valgrind, lint og code-coverage som supplement til compilerens analyser. Jeg roder også med en model-checker til et subset af C i fritiden, lidt ala SPIN.

@Erlo
I min erfaring er god rekruttering absolut at foretrække. Der er endog meget stor forskel på at have to virkeligt gode programmører vs. to hold af middelmådige 'comodity programmers'. De gode programmører har det talent, der med et moderne begreb kaldes 'computational thinking', i meget stor grad og der virker sprog som C som en forstærkning af evnerne, mens tungere sprog, der foretrækkes af programmerings'fabrikker' og PHB'ere snarere virker som en hæmsko.
ADA har bestemt nogle fortrin og har nok ikke tiltrukket helt så mange 'commodity programmers' som andre mere populære sprog - ingen nævnt, ingen glemt. ;)

@Jens
Jeg har som mange andre også brugt timer på at finde mystiske fejl og decifrerer compiler output. Trods det køber jeg ikke den præmis jeg læste om at MISRA-C skal gøre det lettere for den urutinerede programmør. Den urutinerede programmør bør hellere lære sin metier ved f.eks. god sidemandsoplæring og simplere opgaver og bør ikke overlades kritisk arbejde, før vedkommende er klar til det.

Enig med Torben.
Der er en del leveregler der gør C mere end ok - bla

ingen malloc/free efter init
brug structs overalt ingen løse arrays osv
ingen typeløse pointere
ingen typecasting på pointers som udgangspunkt, men kan være nødvendig.
fuld hug på compiler warnings
funktionalitet må ikke kopieres - lav en funktion istedet
styr på små og store indianere (big/little endian :-)
brug eks splint og annoter koden
osv osv
indbyg debug/tracing som en del af koden
osv osv

så kør noget gammeldags cyclomatic index mm. Giver faktisk til tider et hint om hvor der skal simplificeres i koden.

Man skal huske på at mange systemer stadig er å 8/16 bit micros hvor der ikke er resoucer til at mange checks og hvor der ingen MMU er.

Det er et håndværk man kun kan lære på een måde.