2 पॉइंट द्वारा GN⁺ 24 일 전 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • 57 वर्षों तक लगभग परफेक्ट माना गया Apollo Guidance Computer(AGC) कोड में resource unlock छूट जाने वाला bug मिला है
  • JUXT टीम ने AI specification language Allium और Claude का उपयोग करके 1.3 लाख lines की assembly का विश्लेषण किया और ऐसा defect पहचाना जो पारंपरिक verification तरीकों से सामने नहीं आया था
  • gyro control routine के abnormal termination path (BADEND) में LGYRO lock release नहीं होता, जिससे बाद की सभी gyro-संबंधित functions रुक सकती हैं
  • अगर वास्तविक मिशन के दौरान चंद्र कक्षा में Cage switch गलती से दब गया होता, तो Program 52 alignment रुक सकता था और Collins इसे hardware failure समझ सकते थे
  • यह मामला दिखाता है कि behavior-specification-based analysis पुराने कोड में भी नए defects खोजने का एक शक्तिशाली तरीका है

Apollo 11 Guidance Computer में मिला संभावित defect

  • Apollo Guidance Computer(AGC) इतिहास के सबसे गहराई से जांचे गए codebases में से एक है, जिसे अनेक developers और researchers ने विश्लेषित किया है
    • फिर भी 57 वर्षों तक नहीं मिला resource lock छूट जाने वाला bug gyro control code में पाया गया
    • error path में lock release न होने से guidance platform की realignment function निष्क्रिय हो सकती थी
  • JUXT टीम ने AI-आधारित specification language Allium और Claude का उपयोग करके AGC की 1.3 लाख lines assembly को 12,500 lines की behavioral specification में बदला
    • कोड से सीधे specification निकालकर resource acquisition और release के सभी paths को model किया गया
    • इसी प्रक्रिया में ऐसा defect सामने आया जो सामान्य code reading या emulation से नहीं दिखता था

कोड संरचना और विश्लेषण का तरीका

  • AGC source 2003 में Ron Burkey और volunteers ने MIT Instrumentation Laboratory की printed copies को हाथ से transcribe करके सार्वजनिक किया
    • 2016 में Chris Garry का GitHub repository सामने आया, जिसके बाद दुनिया भर के developers ने 2KB RAM और 1MHz CPU पर चलने वाले assembly code का अध्ययन किया
  • प्रोग्राम 74KB की core rope memory में store था, जिसमें copper wires को magnetic cores में हाथ से बुनकर 1 और 0 व्यक्त किए जाते थे
    • यह काम करने वाली महिला technicians को “Little Old Ladies” कहा जाता था, और memory का नाम LOL memory पड़ा
  • अब तक AGC पर formal verification, model checking, static analysis किए जाने का कोई रिकॉर्ड नहीं था
    • अधिकांश verification code reading, emulation, और transcription accuracy की जांच पर केंद्रित थी
  • JUXT ने IMU(Inertial Measurement Unit) subsystem की behavioral specification Allium में लिखी
    • हर shared resource के acquire/release timing को model करके defect पहचाना गया

gyro control routine में lock release का छूटना

  • AGC, IMU को LGYRO नाम के shared lock से manage करता है
    • gyroscope को torque करते समय lock लिया जाता है, और तीनों axes पूरे होने पर release किया जाता है
    • इससे एक ही समय में दो routines द्वारा hardware manipulation रोकी जाती है
  • लेकिन abnormal termination path में lock release नहीं होता
    • normal exit पर STRTGYR2 routine LGYRO release करती है, लेकिन ‘Caging’ (gyro की सुरक्षा के लिए physical lock) होने पर control BADEND routine में चला जाता है
    • BADEND में CAF ZERO और TS LGYRO ये दो instructions (कुल 4 bytes) नहीं हैं, इसलिए lock बना रहता है
  • LGYRO release न होने पर बाद की सभी gyro torque routines lock-wait state में रुक जाती हैं
    • fine alignment, drift correction, manual torque जैसी सभी gyro-संबंधित functions ठप हो सकती हैं

चंद्रमा के पीछे की ओर संभावित प्रभाव

  • 21 जुलाई 1969 को Michael Collins चंद्र कक्षा में समय-समय पर Program 52 (star-sighting alignment program) चलाते थे
    • अगर platform drift करता, तो return engine की दिशा गलत होने का जोखिम था
  • अगर torque के दौरान गलती से Cage switch दब जाता और control BADEND path में चला जाता, तो LGYRO release न होने से बाद के सभी P52 रुक सकते थे
    • DSKY (display-keyboard) input तो लेता, लेकिन response नहीं देता
    • बाकी functions सामान्य दिखतीं, इसलिए Collins इसे hardware failure समझ सकते थे
  • यदि restart (hard reset) किया जाता, तो समस्या हल हो जाती, लेकिन चंद्र अवतरण के दौरान आए 1202 alarm के अनुभव को देखते हुए तुरंत reset का निर्णय लेना कठिन हो सकता था

मौजूदा सिस्टम की defensive design और उसकी सीमाएँ

  • Margaret Hamilton के नेतृत्व वाली MIT टीम ने priority scheduling, asynchronous multitasking, restart protection जैसे आधुनिक software engineering के बुनियादी concepts पेश किए
    • इसी design की वजह से 1202 alarm के दौरान भी landing संभव हो सकी
  • अधिकांश बड़े defects specification errors थे, और Don Eyles द्वारा documented उदाहरणों की तरह hardware के बीच phase synchronization की कमी से CPU load बढ़ा था
  • यह defect भी कुछ वैसी ही संरचना का है
    • BADEND IMU mode switch का सामान्य termination routine है, जो MODECADR जैसे common resources तो release करती है, लेकिन LGYRO को नहीं संभालती
    • क्योंकि restart logic LGYRO को initialize कर देता है, इसलिए testing के दौरान recovery हो जाती थी और defect छिपा रहता था
  • लेकिन बिना restart वाली वास्तविक स्थिति में gyro स्थायी locked state में रह सकता था

Allium के जरिए defect खोजने की प्रक्रिया

  • Allium specification हर resource के lifecycle को model करती है
    • gyros_busy field LGYRO को दर्शाती है, और GyroTorque rule lock acquisition को, जबकि GyroTorqueBusy rule पहले से locked होने पर wait state को परिभाषित करता है
  • specification यह obligation तय करती है कि “अगर lock true हो जाए, तो उसे अनिवार्य रूप से false पर वापस आना चाहिए”
    • Claude ने सभी paths को trace किया और पाया कि normal path (STRTGYR2) में release होता है, लेकिन error path (BADEND) में नहीं
  • specification-based approach यह verify करती है कि कोड क्या करना चाहिए, न कि सिर्फ क्या कर रहा है
    • testing वर्तमान behavior की पुष्टि करती है, जबकि specification intended behavior को verify करती है
  • Allium specification और bug reproduction code GitHub पर सार्वजनिक हैं

आधुनिक संदर्भ और सीख

  • उस समय programmers को CAF ZERO और TS LGYRO instructions के जरिए lock manually release करना पड़ता था
    • उन्हें हर path याद रखना पड़ता था और manually release code डालना होता था
  • आधुनिक languages ऐसी resource leak समस्याओं को संरचनात्मक रूप से रोकती हैं
    • Go का defer, Java का try-with-resources, Python का with, Rust का ownership system automatic release सुनिश्चित करते हैं
  • फिर भी CWE-772 (Missing Release of Resource after Effective Lifetime) प्रकार के defects आज भी मौजूद हैं
    • database connections, distributed locks, file handles, infrastructure shutdown order जैसी चीज़ें अब भी programmer की जिम्मेदारी रहती हैं
  • Apollo missions सभी सफलतापूर्वक लौट आए, लेकिन यह defect बाद के COMANCHE (command module) और LUMINARY (lunar module) software में भी जस का तस मौजूद रहा और कभी fix नहीं हुआ
  • 57 वर्षों तक छिपा रहा यह defect behavior-specification-based analysis के महत्व को दिखाने वाला उदाहरण है

1 टिप्पणियां

 
GN⁺ 24 일 전
Hacker News टिप्पणियाँ
  • मैं Mike Stewart हूँ, और CuriousMarc चैनल पर AGC restoration project का नेतृत्व किया था तथा VirtualAGC का co-maintainer हूँ
    यहाँ जिस bug का ज़िक्र है, वह वास्तव में AGC software में मौजूद defect था। लेकिन पूरे program के दौरान उसे अनदेखा नहीं किया गया था। यह SATANCHE के phase 3 test के दौरान मिला, L-1D-02 के रूप में दर्ज किया गया, और Apollo 14 और 15 के बीच ठीक कर दिया गया
    संबंधित reports ibiblio document 1 और document 2 में देखी जा सकती हैं
    fix सिर्फ LGYRO को 0 बनाने वाली दो lines जोड़ना नहीं था, बल्कि इसमें code structure का पुनर्गठन और pending tasks को जगाने वाला logic भी शामिल था। Apollo 14 और 15 के code की तुलना करें (Apollo 14 code, Apollo 15 code) तो फर्क दिखेगा
    यह article में बताए गए तरीके से चुपचाप होने वाला bug नहीं है। LGYRO, STARTSB2 में भी initialize होता है, जो हर बार program switch पर चलता है और समस्या को अपने-आप साफ कर देता है। इसलिए व्यवहार में यह सिर्फ BADEND के दौरान torque operation करते समय ही कभी-कभार होता था
    अगर bug बना रहता, तो कई tasks जमा हो जाते और अंततः 31202 error (1202 का बाद का version) पैदा होता। यह समस्या Apollo 14 flight से पहले पकड़ ली गई थी, इसलिए Apollo 14 Program Notes में recovery procedure जोड़ा गया था
    साथ ही, Ken Shirriff ने gate-level analysis किया बताया जाता है, लेकिन वास्तव में उसका अधिकांश काम मैंने किया था
    Virtual AGC ने सिर्फ कुछ programs के लिए original core rope dump के साथ byte-level exact match verification पूरी की है; पूरे program के लिए यह अभी संभव नहीं है। ज़्यादातर source printouts या checksums के आधार पर restore किया गया है
    Margaret Hamilton, Comanche (command module software) की ‘rope mother’ थीं, और Luminary (lunar module) के लिए Jim Kernan ज़िम्मेदार थे। यह 1969 organizational chart में देखा जा सकता है
    1202 alarm के समय AGC को low-priority tasks हटाने के लिए design नहीं किया गया था। बल्कि landing guidance ही सबसे low-priority task था, और antenna control तथा display refresh उससे ऊँची priority पर थे। इस document में हर task की priority दी गई है
    और अंत में, 1202 alarm का कारण phase difference नहीं बल्कि voltage difference (28V vs 15V) था, यह वास्तविक hardware tests में पुष्टि हो चुका है। संबंधित experiment video YouTube link पर देखा जा सकता है

    • मैं आपकी comment का इंतज़ार कर रहा था। इतने शानदार ऐतिहासिक विवरण साझा करने के लिए धन्यवाद
    • main page अब किसी और topic पर आगे बढ़ चुकी है, लेकिन यह सच में खज़ाने जैसी जानकारी है। समय निकालने के लिए आभारी हूँ
  • अगर Apollo AGC में रुचि है, तो मैं ज़रूर CuriousMarc YouTube channel देखने की सलाह दूँगा। एक तकनीकी रूप से बेहद मजबूत टीम AGC के कई components को restore और analyze करने की प्रक्रिया दर्ज कर रही है
    खास तौर पर दिलचस्प हिस्सा बदनाम 1202 alarm की पुनर्व्याख्या है। आम तौर पर इसे एक नज़रअंदाज़ करने योग्य sensor error माना जाता है, लेकिन वास्तव में कुछ परिस्थितियों में यह बहुत गंभीर हो सकता था

    • इसलिए कहा जा सकता है कि आज उसी landing को फिर से करने की कोशिश करना कुछ मायनों में ज़्यादा कठिन और कुछ मायनों में आसान है। क्योंकि हमें उस समय की तुलना में कहीं अधिक failure modes मालूम हैं
    • “लोकप्रिय तौर पर समझाई गई बात” और “वास्तव में समझी गई बात” अलग हैं। बहुत-सी explanations simplified हैं, लेकिन experts के बीच यह phenomenon पहले से अच्छी तरह समझा जा चुका है
    • CuriousMarc टीम की AGC restoration पर चर्चा इस thread में भी जारी है
  • मेरा सबसे पसंदीदा code snippet यह है

    TC  BANKCALL  # TEMPORARY, I HOPE HOPE HOPE
    CADR STOPRATE  # TEMPORARY, I HOPE HOPE HOPE
    TC  DOWNFLAG  # PERMIT X-AXIS OVERRIDE
    

    GitHub link

    • इस code का ज़िक्र The Codeless Code में भी है
    • यहाँ CADR का Lisp के cadr function से कोई संबंध नहीं है
    • क्या कोई बता सकता है कि यह code मज़ेदार क्यों है?
    • मुझे याद है कि मैंने कभी XKCD में इस code पर एक कविता देखी थी, हालाँकि शायद मैं गलत भी हो सकता हूँ
  • मुझे जिज्ञासा है कि क्या यह verify किया गया है कि bug सच में मौजूद है। AI इस तरह की exploratory analysis में मजबूत है, लेकिन अब भी इसकी false positive rate ऊँची है
    संदर्भ के हिसाब से यह महत्वपूर्ण भी हो सकता है और नहीं भी। बहुत से bugs ऐसे भी हैं जिन्हें AI पकड़ नहीं पाता
    मेरे पास खुद इसे verify करने की विशेषज्ञता नहीं है, लेकिन यह बहुत रोचक है

    • सच कहें तो यह भी साफ नहीं है कि bug AI ने ही ढूँढा था। बस इतना लिखा है कि “इसे AI native language में model किया गया”
      फिर भी lock acquisition और failure scenario की explanation काफ़ी convincing थी
  • उनका वास्तव में एक bug ढूँढना दिलचस्प है। लेकिन लेख की नाटकीय प्रस्तुति लगभग काल्पनिक लगती है
    जैसे कोहनी से switch छू जाना, या reset से ठीक हो सकने वाली समस्या को बढ़ा-चढ़ाकर दिखाना। ऐसी बातें लेख को sensational बनाती हैं, लेकिन उसकी credibility घटाती हैं। ऊपर से AI द्वारा लिखी गई जैसी शैली इसे और खटकाऊ बनाती है

    • बेशक वह switch protective cover वाला switch था।
      लेकिन आम पाठकों को ऐसा subtle bug समझाने के लिए कुछ हद तक storytelling चाहिए। बहुत technical होगा तो रुचि चली जाएगी, बहुत dramatic होगा तो experts आलोचना करेंगे। मेरा मानना है कि वह संतुलन बनाना कठिन है
  • मैंने article में शामिल repro code खुद चलाकर देखा
    GitHub link
    यह चलता तो है, लेकिन Phase 5 (deadlock demonstration) पूरी तरह fake output है। असली emulator चलाने के बजाय यह सिर्फ expected results print करता है
    इसलिए मैंने खुद एक PR भेजा, जिसमें इसे ठीक किया ताकि यह emulator पर सच में चले, और यह भी verify किया कि दो-line patch bug को हल कर देता है

    • मैं अक्सर इस तरह का “AI code” देखता हूँ। यह test-driven development की नकल करता है, लेकिन वास्तव में सिर्फ tests pass कराने वाला fake code देता है
      AI-generated code अक्सर “अब यह perfect है!” कहकर रुक जाता है, और लोग उस पर भरोसा करके उसे वैसे ही ship कर देते हैं। असली समस्या यही है
  • लेख खुद में दिलचस्प है, लेकिन इसमें LLM द्वारा लिखी गई जैसी कृत्रिम अनुभूति बहुत प्रबल है

    • मुझे इसमें बिल्कुल भी LLM जैसा एहसास नहीं हुआ। शायद इसलिए कि इसकी शैली scientific paper जैसी है
    • Juxt पहले से ही बेहतरीन लेख लिखता आया है, और उसकी expertise भी पर्याप्त है। इसलिए मुझे नहीं लगता कि यह लेख AI-generated होने की संभावना रखता है
    • संदर्भ के लिए, Pangram analysis के अनुसार यह लेख मानव द्वारा लिखा गया माना गया है
    • लेकिन Juxt की दूसरी posts में से एक में वास्तव में Claude द्वारा लिखा गया होने की बात साफ़ कही गई है। यह उस लेख के आख़िरी paragraph में बताया गया है
    • इसके अलावा Rust और locks से जुड़ा हिस्सा तथ्यात्मक रूप से गलत है। यह इस comment में बताया गया है
  • सिर्फ 4KB memory के साथ इंसान को चाँद पर भेजने वाले software में अब भी अभी तक न मिले bugs हो सकते हैं, यह दिखाता है कि छोटे code में भी complexity छिपी हो सकती है

    • memory जितनी कम होती है, code length और bug rate का संबंध उतना ही कमज़ोर हो जाता है। बल्कि complexity को compress करने की कोशिश में bugs बढ़ जाते हैं
    • यह बात मुझे बस एक खाली घिसी-पिटी पंक्ति जैसी लगती है
  • “code से specification निकाला गया” कहना गलत है। specification का मतलब फिर से देखना चाहिए

    • दरअसल उसका मतलब सिर्फ reverse engineering है
  • article और repository, दोनों ही कम गुणवत्ता वाले sloppy output हैं
    repository link को देखें तो, “repro” कहते हुए भी वह असली bug नहीं चलाता, बल्कि सिर्फ “ऐसा होगा” जैसे print statements दिखाता है