- 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 के महत्व को दिखाने वाला उदाहरण है
अभी कोई टिप्पणी नहीं है.