لینک کوتاه مطلب : https://hsgar.com/?p=5854

تنظیمات کاربر، ساعت های Lamport و روش های رسمی سبک

همگام سازی تنظیمات بین مرورگرها و یک backend کار ساده ای به نظر می رسد. به نظر می رسد که می تواند درس هایی در مورد سیستم های توزیع و مدل سازی رسمی به ما بیاموزد. پس از خواندن این پست، امیدوارم نحوه استفاده ما را یاد بگیرید
ساعت های لامپورت برای همگام سازی تنظیمات کاربر بین مرورگرها و خدمات باطن. همچنین نحوه استفاده ما را یاد خواهید گرفت روش های رسمی سبک وزن برای یافتن اشکالات در اجرای پروتکل همگام سازی ما.

در هوش فضایی ما روی محصولاتی کار می کنیم که از عملیات خطوط هوایی پشتیبانی می کنند. یکی از محصولاتی که ما در حال ساخت آن هستیم، اپلیکیشنی برای ارسال پیام بین دیسپچرها (کارکنان زمینی هماهنگ کننده هواپیماهای حامل) و خلبانان (افرادی که هواپیماها را هدایت می کنند) است. به WhatsApp برای هواپیما فکر کنید.

برنامه، یا فقط برنامه، با آن ادغام می شود سیستم های خطوط هوایی موجود. این برنامه رابط کاربری نرم‌افزار مرورگر را ارائه می‌کند، و در عین حال باید با سیستم‌های اعلان موجود ارتباط برقرار کند تا از ارسال پیام جدیدی از طرف خلبان مطلع شود. «سیستم‌های اطلاع‌رسانی موجود» مبتنی بر مرورگر نیستند، بنابراین حتی اگر پیام‌رسانی خود در مرورگر اتفاق می‌افتد، جریان اعلان خارج از مرورگر اتفاق می‌افتد. به اعلان‌های فشاری فکر کنید که به دستگاهی خارج از مرورگر تحویل داده می‌شوند. برای ارائه پیام‌ها به کاربران مناسب (مثلاً همه توزیع‌کنندگان علاقه‌مند به پروازهایی که از سیاتل حرکت می‌کنند)، سرویس پشتیبان به تنظیمات کاربر متکی است تا بفهمد که کدام کاربر (فرستنده) باید در مورد کدام پیام مطلع شود. دیسپچرهای مختلف مجموعه متفاوتی از پروازها را انجام می دهند.

مهم است که مرورگرهایی که برنامه را ارائه می‌کنند، متصل به باطن و خود بک‌اند، دید ثابتی نسبت به تنظیمات کاربر داشته باشند، بنابراین بک‌اند می‌تواند به طور قابل‌اطمینانی اعلان‌های ارسال پیام‌های معلق را به توزیع‌کنندگان ارسال کند. موردی که ما به‌ویژه می‌خواهیم از آن اجتناب کنیم این است که مرورگرها تنظیمات متفاوتی را نسبت به تنظیمات پشتیبان‌شده «می‌بینند» یا اینکه تنظیمات بین مرورگرها و backend همگرا نمی‌شوند. در عین حال، می‌خواهیم تجربه‌ای جذاب را ارائه دهیم، زمانی که دیسپاچر می‌تواند تنظیمات مختلف (انتخابگرهای پرواز مختلف) را انتخاب کند و تنظیمات سوسو نمی‌زند زیرا درخواست‌ها و پاسخ‌ها بین مرورگر و باطن به عقب و جلو می‌روند.

ظاهرا بله. اما اگر می خواهید باشید مطمئن اینکه تنظیمات به درستی همگام‌سازی شده‌اند، از حاشیه‌های عجیب و غریب اجتناب کنید و همچنان تجربه‌ای سریع را ارائه دهید، باید مراقب بیشتری باشید.

با دو مرورگر و یک بک‌اند (تک ذخیره‌سازی)، اتفاقات مختلفی می‌تواند رخ دهد. کاربر می‌تواند روی تنظیمات در یک مرورگر کلیک کند و سپس تنظیمات مختلف را در مرورگر دیگر کلیک کند. ممکن است مشکلات شبکه گذرا وجود داشته باشد، بنابراین مرورگرها نمی توانند تنظیمات به روز را به باطن ارسال کنند. کاربر می تواند چندین بار روی تنظیمات کلیک کرده و یا مرورگر را مجددا راه اندازی کند.

ساده ترین کار ارسال تنظیمات با هر کلیک است. مشکل این است که اگر تنظیمات مختلف را سریع کلیک کنید، یا زمانی که شبکه کند است، ممکن است برخی از تنظیمات A و سپس تنظیمات دیگری B را تغییر دهید، اما پس از کلیک بر روی B، مرورگر شما پاسخی از پشتیبان برای “A” دریافت کرد. ” تغییر دادن. “پاسخ A” تغییر “B” را در مرورگر بازنویسی می کند و باعث سوسو زدن تنظیمات می شود. متناوباً، می‌توانید پس از هر درخواست منتظر پاسخ باشید، اما پس از آن، این تجربه «سریع» نخواهد بود.

همچنین، اگر درخواست شما هرگز به سرویس پشتیبان نرسید چه؟ آها، شما می گویید، بیایید یک کار همگام سازی دوره ای را در مرورگر اضافه کنیم تا وضعیت مرورگر با backend همگام شود. این همچنین از ما در برابر مواردی که شخصی تنظیمات را در پنجره مرورگر دیگری تغییر می‌دهد محافظت می‌کند. این کار می کند، اما شما باید بفهمید که کدام تنظیمات “فعالی” هستند، آنهایی که در مرورگر هستند یا تنظیمات پشتیبان. آسان است، فقط یک ساعت اضافه کنید. اما حالا چطور می توانید باشید مطمئن که ساعت درست است؟ باید، اما اگر نه? چگونه می توانید قابل اعتماد ساعت ها را مقایسه کنید? حکمت عامیانه می گوید هرگز به ساعت های خارجی اعتماد نکنید.

شما می توانید مقداری عدد صحیح اضافه کنید که هر بار که همگام سازی می کنید یا حالت را تغییر می دهید، آن را افزایش می دهید و عدد بزرگتر را انتخاب می کنید… صبر کنید، به نظر می رسد که شما در حال اختراع …

ایده ساده است: کاری کنید که هر فرآیند زمان خود را اندازه گیری کند، و زمانی را که فرآیندها (مرورگرها و باطن) رویدادها را مبادله می کنند، هماهنگ کنید.

رویدادها زمان را “تیک” می کنند. هنگامی که یک رویداد، مانند تغییر در تنظیمات، اتفاق می افتد، یک فرآیند زمان محلی خود را افزایش می دهد (یک عدد صحیح). هنگامی که فرآیندها اطلاعات را مبادله می کنند، شمارنده را به همراه می گذرانند، شمارنده دریافتی را با شمارنده محلی مقایسه می کنند، بزرگتر (محلی یا دریافتی) را همراه با حالت همراه (یعنی تنظیمات) انتخاب می کنند. و ساعت محلی را 1 افزایش دهید. آقای لامپورت نشان داد که چنین ساعت هایی اجازه استدلال در مورد آن را می دهند ترتیب وقایع.

هر بار که کاربر روی تنظیمات کلیک می کند، ساعت Lamport (یک عدد صحیح محلی) در مرورگر 1 افزایش می یابد. تنظیمات از مرورگرها به پشتیبان ارسال می شود و “ساعت بزرگتر برنده می شود”. در نهایت، همه مرورگرها و باطن باید به مقادیر یکسانی همگرا شوند… حداقل این چیزی است که ما فکر می کردیم.

آزمایش یک سیستم توزیع شده، حتی به سادگی موارد بالا، دشوار است. وجود دارد چارچوب‌ها و زبان‌های اختصاصی، مانند TLA+ برای این منظور در حالی که رسا و در جنگ اثبات شده است، یک “تست” یا مشخصات نوشته شده در TLA+ محکوم به عدم نگهداری فوری است. در عوض، ما “آزمایش مبتنی بر ویژگی” را که در قسمت توضیح داده شده است، اتخاذ کردیم
روش های رسمی سبک وزن کاغذ. به طور خلاصه، ایده این است که شما مدل‌های مرجع ساده را پیاده‌سازی کنید، سپس به‌طور تصادفی مجموعه‌هایی از رویدادها را تولید کنید و بررسی کنید که آیا پس از اجرای رویدادها روی مدل‌های مرجع، ویژگی‌های سیستم حفظ می‌شوند یا خیر. چنین «آزمون‌های رسمی سبک وزن»، همراه با سایر آزمون‌ها، بخشی از مجموعه آزمون واحد معمولی هستند.

در مورد ما، یک “مدل مرجع” برای یک برنامه مرورگر صرفا یک کلاس با دو فیلد – “تنظیمات” و “ساعت لامپورت” بود. سرویس پشتیبان مورد استفاده در تست ها عبارت بود از واقعی سرویس باطن که به صورت محلی به عنوان بخشی از راه اندازی تست واحد اجرا می شود.

رویدادهای ایجاد شده عبارت بودند از:

  1. کاربر تنظیمات برنامه را تغییر داد و برنامه تنظیمات به‌روز را به باطن ارسال کرد.
  2. کاربر تنظیمات را تغییر داد اما مرورگر تنظیمات به‌روز را به باطن ارسال نکرد (مثلاً به دلیل مشکلات اتصال).
  3. مرورگر با backend همگام می شود.
  4. مرورگر ریست می شود.

چیزی که ما برای آن آزمایش کردیم این ویژگی بود: پس از مجموعه‌ای تصادفی از رویدادها و دو دور همگام‌سازی بین مرورگرها و باطن، همه مرورگرها و باطن تنظیمات یکسانی داشتند. ما از “دو دور همگام سازی” استفاده کردیم زیرا مشخص شد که یک دور همگام سازی برای همگرایی کافی نیست.

بنابراین ما آزمایش را با هزاران و هزاران دنباله از رویدادها اجرا می کنیم، و در کمال تعجب، آزمایش ها شکست خوردند! توالی وقایع بود که باعث شد سیستم به یک حالت واحد همگرا نشود. مشخص شد که وقتی همه مرورگرها و باطن تنظیمات متفاوتی داشته باشند اما مقادیر یکسان ساعت Lamport داشته باشند، وضعیت همگرا نمی شود. دنباله زیر را در نظر بگیرید:

  1. حالت اولیه
    • مرورگر: تنظیمات: هیچ، ساعت: 0
    • باطن: تنظیمات: هیچ، ساعت: 0
  2. کاربر تنظیمات را در مرورگر تغییر می دهد و مرورگر تنظیمات را با backend همگام می کند. ساعت برای مرورگر 3 است: درست پس از تغییر تنظیمات، ساعت به صورت محلی به 1 افزایش می یابد، به باطن ارسال می شود، باطن ساعت را به 2 افزایش می دهد و آن را به مرورگر می فرستد، جایی که دوباره به 3 افزایش می یابد.
    • مرورگر: تنظیمات: foo، ساعت: 3
    • باطن: تنظیمات: foo، ساعت: 2
  3. مرورگر ریست می شود، تمام حالت حذف می شود.
    • مرورگر: تنظیمات: هیچ، ساعت: 0
    • باطن: تنظیمات: foo، ساعت: 2
  4. کاربر تنظیمات را دو بار تغییر می‌دهد، اما این بار وضعیت به باطن منتشر نمی‌شود (مثلاً به دلیل مشکلات شبکه).
    • مرورگر: تنظیمات: هیچ، ساعت: 2
    • باطن: تنظیمات: foo، ساعت: 2

حال، اگر اینطور باقی بماند، وضعیت هرگز بین مرورگر و باطن همگرا نمی شود. هر دو انتها مقدار ساعت یکسانی دارند و نمی توانند در مورد ترتیب رویدادها تصمیم بگیرند. نادر؟ بله، نادر است. درست؟ قطعا نه!

راه حل این بود که هر زمان که درخواستی با ساعت مساوی ارائه می شود، با افزایش ساعت در سمت باطن، کراوات را شکستیم. به طور شهودی، می توان استدلال کرد که ممکن است در همین حین چیزی در قسمت پشتیبان اتفاق افتاده باشد، به عنوان مثال تنظیمات به مقداری تغییر کرده و به مقدار اصلی تغییر کرده و تنظیمات را بدون تغییر باقی می گذارد اما ساعت افزایش می یابد. با مثال بالا، وقتی backend رویدادی با مقدار ساعت مرورگر برابر با مقدار ساعت محلی backend دریافت می‌کند، backend بی‌صدا ساعت خود را افزایش می‌دهد و آن را به مرورگر برمی‌گرداند:

  1. Backend ساعت خود را در یک ساعت ورودی برابر افزایش می دهد.
    • مرورگر: تنظیمات: هیچ، ساعت: 4
    • باطن: تنظیمات: foo، ساعت: 3

بعد از تغییر، آزمون دیگر شکست نمی خورد.

اگر کسی بخواهد آن را به درستی انجام دهد، مدیریت حتی یک حالت توزیع شده ساده هم بی اهمیت نیست. خوشبختانه الگوریتم ها و تحقیقات غنی وجود دارد. تست رسمی سبک وزن بسیار است کاربردی چارچوبی برای آزمایش چنین الگوریتم هایی در زمینه برنامه.

لینک منبع

ارسال یک پاسخ

آدرس ایمیل شما منتشر نخواهد شد.