Amazon Web Services में सिस्टम सटीकता के व्यावहारिक उदाहरण
(cacm.acm.org)- Amazon Web Services(AWS) सेवा की सटीकता को एक मुख्य मूल्य मानते हुए विकास प्रक्रिया में विभिन्न प्रकार की formal methodologies को एकीकृत करता है
- TLA+ और P भाषा जैसे formal specification tools के माध्यम से सूक्ष्म bugs को शुरुआती चरण में खोजा जा सकता है, और साहसी optimization के दौरान भी reliability सुनिश्चित की जा सकती है
- AWS lightweight formal methodologies के रूप में property-based testing, deterministic simulation, और continuous fuzzing का भी व्यापक उपयोग करता है
- Fault Injection Service जैसे failure injection tools के जरिए failure scenarios सहित reliability verification को स्वचालित किया जाता है
- शैक्षणिक बाधाएँ और tools की जटिलता अब भी बनी हुई हैं, लेकिन AI और automation tools का प्रसार इनके व्यापक अपनाव में मदद कर सकता है
AWS की सिस्टम सटीकता सुनिश्चित करने की रणनीति
Amazon Web Services(AWS) का लक्ष्य ऐसे उच्च-विश्वसनीयता वाले services प्रदान करना है जिन पर ग्राहक पूरी तरह भरोसा कर सकें
इसके लिए AWS security, durability, integrity, availability के मानकों को बनाए रखने का प्रयास करता है, और इसके केंद्र में system correctness की अवधारणा रखता है
2015 में Communications of the ACM में प्रकाशित AWS के formal methodologies के उपयोग के बाद से, यह दृष्टिकोण core services के सफल संचालन में महत्वपूर्ण भूमिका निभाता आ रहा है
इसका केंद्र Leslie Lamport द्वारा विकसित TLA+ नामक formal specification language है
AWS के TLA+ अपनाने के अनुभव ने विकास के शुरुआती चरण में ऐसे सूक्ष्म bugs पहचानने में मदद की, जिन्हें पारंपरिक testing से पकड़ना मुश्किल था
इसके अलावा, आक्रामक performance optimization करते समय भी formal verification के माध्यम से stability और reliability सुनिश्चित की जा सकी
15 साल पहले AWS build-time unit testing और सीमित integration testing जैसे बुनियादी स्तर तक ही सीमित था, लेकिन बाद में इसने formal और semi-formal approaches को व्यापक रूप से अपनाया
इन बदलावों ने न केवल correctness, बल्कि high-level और low-level optimization validation, development speed में सुधार, और cost reduction में भी योगदान दिया
AWS में पारंपरिक formal proof, model checking के अलावा property-based testing, fuzzing, runtime monitoring को भी formal methodologies के दायरे में स्वीकार किया जाता है
P programming language का आगमन
शुरुआत में TLA+ की ताकत उसके शक्तिशाली abstract description में थी, लेकिन अनेक developers के लिए mathematical notation का उपयोग एक बड़ी entry barrier था
इसीलिए AWS ने P language को अपनाया, जो developers को परिचित state machine आधारित approach प्रदान करती है
P भाषा distributed systems के design और analysis के लिए state machine modeling का तरीका देती है
यह microservice-based SOA architecture का उपयोग करने वाले Amazon developers के लिए एक परिचित अवधारणा है
2019 से इसे AWS में विकसित किया जा रहा है और strategic open source project के रूप में प्रबंधित किया जा रहा है
Amazon S3, EBS, DynamoDB, Aurora, EC2, IoT जैसी प्रमुख service teams, system design की correctness verify करने के लिए P का उपयोग करती हैं
जब S3 को मजबूत read-after-write consistency पर ले जाया गया, तब P के जरिए protocol का modeling और verification किया गया, जिससे design के शुरुआती चरण में bugs हटाए गए और optimization भी सुरक्षित रूप से लागू किए गए
2023 में AWS P team ने PObserve tool विकसित किया, जिससे test और production दोनों environments में distributed systems की correctness verify करना संभव हुआ
PObserve execution logs निकालकर specification के अनुसार सही behavior हुआ या नहीं, इसकी post-verification कर सकता है, और design-stage specification तथा actual code implementation के बीच प्रभावी कड़ी बनाता है
Lightweight formal methodologies का विस्तार
Property-based testing
सबसे प्रतिनिधि lightweight formal technique property-based testing है
उदाहरण के लिए, S3 की ShardStore development team विकास चक्र के हर चरण में property-based testing, code coverage आधारित fuzzing, failure injection, और counterexample minimization का संयुक्त उपयोग करती है
यह तरीका developers द्वारा सीधे लिखी गई correctness specifications से जुड़ता है, और debugging efficiency को भी काफी बढ़ाता है
Deterministic simulation
Deterministic simulation testing में distributed system को single-threaded simulator पर चलाया जाता है, जहाँ सभी random factors जैसे scheduling, timing, message order आदि को नियंत्रित किया जा सकता है
इसे specific failure और success scenarios की testing, bug-triggering sequence adjustment, और fuzzing विस्तार जैसे कई तरीकों से लागू किया जाता है
इससे system latency, failure behavior आदि की verification build stage में जल्दी हो जाती है, और testing coverage भी बढ़ती है
AWS ने इस तरह के build-time testing code को shuttle और turmoil open source projects के रूप में सार्वजनिक किया है
Continuous fuzzing
Continuous fuzzing, खासकर code coverage आधारित बड़े पैमाने पर input generation, integration testing चरण में system correctness verify करने के लिए प्रभावी है
उदाहरण के लिए, Aurora Limitless Database के विकास के दौरान SQL queries और transactions को fuzz किया गया, ताकि partitioning logic की correctness को बड़ी मात्रा में random schemas, datasets, और queries बनाकर verify किया जा सके
परिणामों की तुलना non-sharded engine के behavior या SQLancer जैसी विधियों से की जाती है
Fuzzing और failure injection के संयोजन से database की मुख्य properties जैसे atomicity, consistency, isolation verify की जाती हैं
कुछ properties, जैसे automatically generated transactions और isolation, execution history आधारित post-verification के जरिए सुनिश्चित की जाती हैं
Fault Injection Service के जरिए failure injection
2021 में AWS ने Fault Injection Service(FIS) जारी किया, जिससे ग्राहक भी API errors, I/O interruption, instance failures जैसी विभिन्न defect scenarios को वास्तविक या test environment में जल्दी प्रयोग कर सकें
इसके जरिए architecture की availability सुनिश्चित करने, failure resilience की जाँच करने, error cases में उच्च bug density के अंतर को कम करने, और संभावित गंभीर समस्याओं को पहले से खोजने जैसे लाभ मिलते हैं
FIS का व्यापक उपयोग AWS customers के साथ-साथ Amazon के भीतर भी होता है, और उदाहरण के लिए Prime Day की तैयारी के दौरान ही 733 experiments चलाए गए
Error injection, formal specification के साथ जोड़े जाने पर और अधिक प्रभावी हो जाता है
अपेक्षित behavior को formal specification में लिखने के बाद, वास्तविक fault outcomes की उससे तुलना करने पर पारंपरिक log और metric checks की तुलना में अधिक errors पकड़े जा सकते हैं
Metastability और system emergent behavior
Distributed systems में अत्यधिक load या cache exhaustion जैसी स्थितियों के कारण ऐसे असामान्य metastable states में फँसने के मामले बढ़ रहे हैं, जहाँ system अपने आप recover नहीं कर पाता
ऐसी स्थिति में केवल load कम कर देना सामान्य recovery के लिए पर्याप्त नहीं होता, और यह सामान्य error cases की तुलना में कहीं अधिक कठिन होता है
अधिकांश retry-timeout logic भी इस तरह की घटनाओं का कारण बनती है
पारंपरिक formal specifications आमतौर पर safety और liveness पर केंद्रित होती हैं, लेकिन metastability के लिए उससे आगे के विविध emergent behaviors को भी ध्यान में रखना पड़ता है
AWS, TLA+ और P जैसे specification models के आधार पर discrete event simulation चलाता है, जिससे performance SLA हासिल होने की संभावना और latency distribution जैसी probabilistic characteristics का व्यवस्थित विश्लेषण किया जा सके
Formal proof की आवश्यकता
कुछ security boundaries (permissions, virtualization आदि) में साधारण testing से आगे बढ़कर mathematical level के proof अनिवार्य होते हैं
उदाहरण के लिए, 2023 में AWS द्वारा अपनाई गई Cedar authorization policy language, Dafny के आधार पर automatic proof और formal verification के लिए अनुकूलित है, और public code तथा correction procedures के माध्यम से सभी उपयोगकर्ता स्वयं भी इसका verification कर सकते हैं
इसी तरह Firecracker VMM की security boundary की key properties पर Kani जैसे Rust code analysis tools से proof कार्य किया जा रहा है
इस प्रकार formal models और specifications को design, implementation, execution, और proof जैसे विभिन्न चरणों में व्यापक रूप से उपयोग करके software correctness सुनिश्चित की जाती है और enterprise तथा customer value बढ़ाई जाती है
Correctness से आगे के अतिरिक्त प्रभाव
Formal methodologies reliability और performance improvement दोनों में महत्वपूर्ण भूमिका निभाती हैं
उदाहरण के लिए, Aurora के commit protocol को P और TLA+ से verify किया गया, जिससे network round trips कम हुए और साथ ही safety भी सुनिश्चित हुई
RSA encryption algorithm के ARM Graviton 2 optimization में, HOL Light में transformation की mathematical correctness साबित की गई, जिससे performance और infrastructure cost दोनों में सुधार जैसा व्यावहारिक लाभ मिला
भविष्य की चुनौतियाँ और अवसर
15 वर्षों में AWS ने उद्योग में formal और semi-formal methodologies के उपयोग का दायरा काफी बढ़ाया है, लेकिन learning curve, विशेषज्ञों की आवश्यकता, और tools की academic प्रकृति जैसी वास्तविक adoption barriers अब भी मौजूद हैं
Property-based testing और deterministic simulation जैसी तकनीकें भी कई developers के लिए अब भी अपरिचित हैं
शिक्षा से जुड़ी entry barriers undergraduate स्तर से ही मौजूद हैं, इसलिए tools और methodologies का प्रसार तथा practical adoption धीमा बना हुआ है
Metastability जैसी large-scale systems की emergent characteristics पर शोध भी अभी शुरुआती चरण में है
आगे चलकर AI/large language models formal models और specifications लिखने में सहायता कर सकते हैं, जिससे practitioners के लिए accessibility कम समय में बहुत अधिक बढ़ने की उम्मीद है
निष्कर्ष
मजबूत और सुरक्षित software बनाने के लिए system correctness सुनिश्चित करने के कई साधनों की आवश्यकता होती है
AWS ने standard testing techniques के अलावा model checking, fuzzing, property-based testing, failure injection testing, deterministic/event-based simulation, और execution history verification जैसी विधियों को व्यापक रूप से अपनाया है
Formal specifications और methodologies, AWS की development process में महत्वपूर्ण test oracle की भूमिका निभाती हैं, और अपने व्यावहारिक तथा आर्थिक प्रभाव सिद्ध कर चुकी हैं, इसलिए वे अब निवेश के प्रमुख क्षेत्रों में शामिल हो चुकी हैं
1 टिप्पणियां
Hacker News की राय
मैं deterministic simulation testing तरीके के बारे में बात करना चाहता/चाहती हूँ। AWS में distributed systems को single-threaded simulator में चलाते हुए thread scheduling, timing, message delivery order जैसी सभी non-deterministic चीज़ों को नियंत्रित किया जाता है। फिर किसी खास failure या success scenario के लिए tests लिखे जाते हैं, और system के भीतर की non-determinism को test framework नियंत्रित करता है। डेवलपर उन specific orders को भी तय कर सकता है जिन्होंने पहले bugs पैदा किए थे। Scheduler को order fuzzing या सभी possible orders की exploration तक भी बढ़ाया जा सकता है। सोच रहा/रही हूँ कि क्या ऐसा कोई language-agnostic open source library है जो यह काम करती हो। विचार यह है कि container के भीतर networking, storage आदि को भी test के समय "deterministic" बनाने वाला middleware tool होना चाहिए। antithesis लगभग यही भूमिका निभाता है, लेकिन मैंने इसे अभी तक open source में नहीं देखा। अगर tests अच्छे लिखे जाएँ तो I/O जैसी चीज़ों को stub करके कुछ हद तक यह हल किया जा सकता है, लेकिन यह मान लेना ठीक नहीं कि हर कोई tests अच्छी तरह लिखता है। मुझे लगता है कि application के ऊपर एक higher layer पर determinism देना अच्छा होगा। दूसरी ओर, उम्मीद है कि AI testing में सचमुच चमक दिखा सकेगा। prompt (requirements) - test implementation - AI - executable code, ये तीनों आदर्श रूप से एक-दूसरे से जुड़ सकते हैं। उम्मीद है AI formal verification को आसान बनाकर software की दुनिया को और अधिक rigorous बनाएगा
deterministic simulation testing (DST) तकनीक के फैलाव में दो मुश्किलें हैं। पहली, पहले यह ज़रूरी था कि पूरे system को किसी specific simulation framework पर सीधे चलाया जाए और दूसरी dependencies न हों। दूसरी, अगर input generation और exploration कमजोर हो, तो सारे tests सफल दिखते हैं लेकिन असल verification नहीं होता। antithesis इन दोनों समस्याओं को हल करने की कोशिश कर रहा है, लेकिन अभी भी बहुत कठिनाइयाँ हैं। ऐसा कोई पक्का तरीका बहुत कम जगहों पर है जिससे determinism किसी भी software पर लागू की जा सके। Facebook का Hermit project भी deterministic Linux userspace के रूप में एक प्रयास था, लेकिन आखिरकार बंद हो गया। deterministic computer testing के अलावा भी बहुत उपयोगी तकनीकी आधार है, और लगता है कि कभी न कभी कोई इसे open source में जारी करेगा
QEMU को 100% emulation mode में single thread पर चलाकर deterministic machine पाना अपेक्षाकृत आसान लगता है। लेकिन असल में जो चाहिए वह है 'controlled' deterministic execution, और यह कहीं ज़्यादा कठिन है। कई processes को किसी तय scenario के अनुसार चलाना हो तो खासकर CPU और OS scheduler level पर कठिनाई बहुत बढ़ जाती है। language-agnostic environment बनाना भी मुश्किल है और छोटी-छोटी details में फँस जाना आसान है। मैंने भी कभी एक simple system बनाया था जो कई JVM threads को खास execution points पर lockstep में चलाता था, और I/O व system time को stubs और control से संभालता था। इस तरह asynchronous components के बीच अलग-अलग interactions, I/O failures, retries आदि test किए, और production में जाने से पहले परेशान करने वाले bugs पकड़ लिए। हालांकि, पूरे system को नियंत्रित करने के बजाय केवल कुछ synchronization points को सरल बनाकर यह संभव हुआ। synchronization mistakes से होने वाले सामान्य data races इस तरीके से पकड़ना मुश्किल है
FoundationDB के testing method की आधिकारिक documentation और YouTube प्रस्तुति वीडियो साझा कर रहा/रही हूँ
अगर भाषा को gdb से debug किया जा सकता है, तो https://rr-project.org/ project की सिफारिश है
याद है कि मैंने पहले Joe Armstrong का एक प्रस्तुति देखी थी जिसमें property testing का उपयोग करके Dropbox को test किया गया था
मुझे लगता है S3 अब तक देखे गए software में सबसे शानदार चीज़ों में से एक है। कुछ साल पहले पूरे S3 system में strong read-after-write consistency जोड़ना भी मुझे वास्तविक software engineering की पराकाष्ठा लगा था blog post link
मैंने S3 lifecycle पर सीधे काम किया है, और वह समय index team द्वारा इस consistency को देने वाली architecture को नए सिरे से design करने के दौर से मेल खाता था। बाहर से देखने पर भी S3 प्रभावशाली है, लेकिन अंदर से implementation और organizational structure दोनों ही कल्पना से परे प्रभावशाली हैं
Google Cloud Storage में तो यह feature (strong consistency) S3 से बहुत पहले से था। कुल मिलाकर GCS थोड़ा ज़्यादा systematic और बेहतर बना हुआ product लगता है
92% वाला आँकड़ा (cluster failures का अधिकांश हिस्सा मामूली failures से शुरू होता है) बहुत सही लगता है। ज़्यादातर मामलों में कोई चमकदार बड़ी दुर्घटना नहीं होती, बल्कि "कोई बड़ी बात नहीं" जैसी retries state accumulation तक पहुँचती हैं और आखिरकार रात 2 बजे बड़े outage में बदल जाती हैं। ऐसे failures पर जो नज़र नहीं आते, उन पर ज़्यादा engineering time लगाना महत्वपूर्ण है
यह मुझे सचमुच बहुत दिलचस्प लेख लगा। infrastructure control plane बनाने में state machine का उपयोग ज़रूरी है। यह ज़रूरी था या नहीं कि P भी चाहिए, इस पर निश्चित नहीं हूँ। हमने भी 13 साल से अधिक समय तक Ruby में infrastructure control plane बनाया है, और यह बहुत बढ़िया काम करता है संबंधित अनुभव साझा करने वाला ब्लॉग
P language के बारे में मेरी जिज्ञासा थी। पहले लगता था कि Microsoft Windows USB stack runtime के लिए P से C code generate करके वास्तव में उसका उपयोग करता था, लेकिन अब शायद production code generation के लिए इसका उपयोग नहीं होता। इस बारे में मैंने Hacker News पर भी प्रश्न छोड़ा था question link। अगर generated code kernel तक जा सकता है, तो अधिक relaxed conditions वाले cloud environments में भी इसका उपयोग निश्चित रूप से संभव होना चाहिए
AWS पृष्ठभूमि न होने और TLA+ या P से परिचित न होने की स्थिति में, अगर कोई "hello world" जैसा उदाहरण होता तो समझना थोड़ा आसान होता। लेख पढ़कर यह प्रक्रिया बस कष्टदायक लग सकती है, और यह भी महसूस हो सकता है कि क्या अच्छे design और testing से ही ये समस्याएँ नहीं पकड़ी जा सकतीं। कोई simple example होता तो यह समझने में मदद मिलती कि वास्तव में किया क्या जा रहा है
TLA+ का एक quick demo example है जो मुझे पसंद है gist link। इसमें कई threads एक shared counter को non-atomically increment करते हैं, और property verification के दौरान race condition पकड़ी जाती है। व्यवहार में ऐसे bugs को केवल testing से ढूँढना बहुत कठिन होता है। ज़्यादातर TLA+ specs इससे कहीं अधिक जटिल होती हैं, लेकिन simple errors पकड़ने के लिए यह example अच्छा है
मैंने खुद TLA इस्तेमाल किया है, लेकिन graphical tool tutorial के साथ ठीक से मेल नहीं खाता था, जिससे निराशा हुई। मैं TLA का उपयोग करना चाहता/चाहती था/थी, और Lamport के काम (LaTeX से लेकर papers तक) को लंबे समय से पसंद करता/करती आया/आई हूँ
formal methods इस्तेमाल करने का मूल आधार यही है कि केवल testing से कभी भी सभी समस्याएँ नहीं पकड़ी जा सकतीं
आधिकारिक TLA+ Examples GitHub repository की सिफारिश है। DieHard problem जैसी सरल चीज़ से शुरू करना अच्छा रहेगा
testing किसी implementation की correctness को किसी problem के specific instances पर साबित करती है, जबकि formal verification पूरी category पर proof देता है। उदाहरण के लिए, अगर कोई function anagrams लौटाता है, तो testing केवल कुछ word pairs के साथ पुष्टि करेगी, लेकिन सभी word pairs पर correctness साबित करने के लिए formal verification चाहिए। undefined behavior या library bugs जैसी कई चीज़ें भी केवल formal verification के दौरान ही पकड़ में आती हैं
"property-based testing, fuzzing, runtime monitoring जैसी lightweight semi-formal techniques" वाली बात पर, मुझे लगता है property-based testing और fuzzing को formal methods का subset कहना ठीक है, लेकिन runtime monitoring को भी semi-formal techniques में शामिल करना थोड़ा ज़्यादा लगता है
पहले Leslie Lamport के साथ Buridan's Principle जैसे papers के कारण कुछ संवाद हुआ था। आज उनकी homepage पर TLA+ और PlusCal के बारे में बहुत कुछ जाना Peterson example page। गणित को programming में लाना, concurrency systems क्षेत्र के शुरुआती अग्रदूतों में होना, system design language (TLA+) बनाना, और उसका AWS जैसी जगहों पर उपयोग होना—यह सब बहुत स्वाभाविक लगता है। इच्छा है कि distributed systems बनाने वाले लोग Lamport की चीज़ों का और अधिक उपयोग करें। large-scale systems में correctness proof बहुत महत्वपूर्ण है
मौजूदा code से TLA+ spec conversion के लिए Claude Opus (Extended Thinking) काफ़ी उपयोगी है। Rust projects और C++ core components की verification में भी इससे कई bugs मिले हैं। दूसरे models अक्सर syntax और spec logic पर अटक जाते हैं, जबकि Opus कहीं अधिक smoothly काम करता है
केवल large-scale systems ही नहीं, बल्कि SSH, terminal जैसी छोटी लेकिन महत्वपूर्ण utilities में भी correctness proof बेहद लाभदायक है, जिनका उपयोग पूरी दुनिया में होता है
"system की correctness proof" वाली बात पर, वास्तव में सब कुछ prove करना संभव नहीं है। model checker केवल इतना बता सकता है कि सीमित state space के भीतर लिखा गया spec कुछ properties को satisfy करता है
व्यक्तिगत रूप से जानना चाहता/चाहती हूँ कि क्या किसी ने distributed service experiments के लिए FIS का उपयोग किया है। इसे अपनाने पर विचार कर रहा/रही हूँ, लेकिन बड़े पैमाने पर experiments का प्रत्यक्ष अनुभव नहीं है
क्या Promela और SPIN लेख में चर्चा की गई चीज़ों से higher-level languages हैं, यह भी जानना चाहता/चाहती हूँ