Complete ARM64 LSE atomic memory semantics across execution backends

.github/workflows/windows-alignment-oracle.yml

@@ -14,6 +14,11 @@ on:
       - 'unittests/emulation/AArch64ExclusiveCases.def'
       - 'unittests/emulation/fixtures/aarch64_exclusive*'
       - 'unittests/emulation/fixtures/AArch64ExclusiveOracle.def'
+      - 'scripts/check_aarch64_atomics.py'
+      - 'scripts/tests/test_check_aarch64_atomics.py'
+      - 'unittests/emulation/AArch64AtomicCases.def'
+      - 'unittests/emulation/fixtures/aarch64_atomic*'
+      - 'unittests/emulation/fixtures/AArch64AtomicOracle.def'
   push:
     branches: [dev]
     paths:
@@ -27,6 +32,11 @@ on:
       - 'unittests/emulation/AArch64ExclusiveCases.def'
       - 'unittests/emulation/fixtures/aarch64_exclusive*'
       - 'unittests/emulation/fixtures/AArch64ExclusiveOracle.def'
+      - 'scripts/check_aarch64_atomics.py'
+      - 'scripts/tests/test_check_aarch64_atomics.py'
+      - 'unittests/emulation/AArch64AtomicCases.def'
+      - 'unittests/emulation/fixtures/aarch64_atomic*'
+      - 'unittests/emulation/fixtures/AArch64AtomicOracle.def'
 
 permissions:
   contents: read
@@ -72,6 +82,18 @@ jobs:
         run: python -m unittest scripts.tests.test_check_aarch64_exclusives -v
       - name: Collect original ARM64 alignment and permission observations
         run: python scripts/check_aarch64_exclusives.py --output build-arm64-alignment
+      - name: Verify ARM64 atomic observation integrity rules
+        run: python -m unittest scripts.tests.test_check_aarch64_atomics -v
+      - name: Collect original ARM64 atomic observations
+        run: python scripts/check_aarch64_atomics.py --output build-arm64-atomics
+      - name: Preserve original ARM64 atomic observations
+        if: ${{ always() }}
+        uses: actions/upload-artifact@v4
+        with:
+          name: windows-atomics-arm64
+          path: build-arm64-atomics/
+          if-no-files-found: error
+          retention-days: 14
       - name: Preserve original ARM64 native observations
         if: ${{ always() }}
         uses: actions/upload-artifact@v4

docs/ar/architecture.md

@@ -1315,7 +1315,9 @@ fail-closed عندما تكون دلالة التعليمة خارج التغط
 
 يمكن لـ `AuthenticatedSourceFrameLoads` عبور استدعاء موصل البيانات الوصفية عبر `swiftMetadataAccessorSourceCallHint`. يعيد مسارا التصريح استخدام الجدول الحالي المثبت بالمترجم، والمزوّد القوي الدقيق، وواجهة Swift ABI الكاملة للطلب واستجابة البيانات الوصفية. تبقى الاستجابة في سجلين وقواعد تغيير السجلات المتطايرة المعتادة محفوظة؛ وما زالت عمليات spill الخاصة تتطلب إثبات البايتات الواصلة المشترك. لا يمنح ذلك تخطيط القيم أو تأثيرات ذاكرة witness أو استعارة إطار أو نموذج تخصيص ديناميكي للمكدس.
 
-يحدد `AArch64ExclusiveInstructions.def` الترميزات المقبولة، وينفذ `AArch64ExclusiveExecution` انتقالات السجلات والمراقب تحت قفل التنفيذ المادي. يحتفظ `RAMReservation` بهوية التخصيص ويتلقى إشعارات الكتابات المعتمدة من المضيف والعروض المحتفظ بها و`RAMTransaction` وتعليمات السلاسل وكتابات `ENTER` الجزئية السابقة للخطأ. لا تُبطل الكتابات المؤقتة والتراجع الحجز. التنفيذ مجهول نطاق الكتابة يُبطل الحجوزات القائمة، بينما يتتبع التنفيذ المصرح به النطاقات المنشورة فعليًا. تمسح أخطاء الضيف واعتراضات الخدمات وربط فضاء العناوين المراقب المحلي. تحتفظ مسارات `LDAR[B/H]` و`STLR[B/H]` الأصلية بعقد RAM ذي المحاذاة الطبيعية. يُبطل محوّل Unicorn البرمجي الحجوزات تحفظيًا في خطافات ما قبل الكتابة بعد قبول المراقبين. وبعد التخزين الحصري، يُبطل ترجمات جميع الأسماء البديلة القابلة للتنفيذ قبل متابعة التشغيل نفسه. يختار `AArch64ExclusiveAccess` سياسة المحاذاة: FEAT_LSE2 لملفات checked ونموذج المحرك لـ Unicorn البرمجي. تعتمد المطابقة على عرض المعامل ووحدة الحجز المادية.
+يحدد `AArch64ExclusiveInstructions.def` الترميزات المقبولة، وينفذ `AArch64ExclusiveExecution` انتقالات السجلات والمراقب تحت قفل التنفيذ المادي. يحتفظ `RAMReservation` بهوية التخصيص ويتلقى إشعارات الكتابات المعتمدة من المضيف والعروض المحتفظ بها و`RAMTransaction` وتعليمات السلاسل وكتابات `ENTER` الجزئية السابقة للخطأ. لا تُبطل الكتابات المؤقتة والتراجع الحجز. التنفيذ مجهول نطاق الكتابة يُبطل الحجوزات القائمة، بينما يتتبع التنفيذ المصرح به النطاقات المنشورة فعليًا. تمسح أخطاء الضيف واعتراضات الخدمات وربط فضاء العناوين المراقب المحلي. تحتفظ مسارات `LDAR[B/H]` و`STLR[B/H]` الأصلية بعقد RAM ذي المحاذاة الطبيعية. يُبطل محوّل Unicorn البرمجي الحجوزات تحفظيًا في خطافات ما قبل الكتابة بعد قبول المراقبين. وبعد التخزين الحصري، يُبطل ترجمات جميع الأسماء البديلة القابلة للتنفيذ قبل متابعة التشغيل نفسه. يختار `AArch64AtomicAccess` سياسة المحاذاة: FEAT_LSE2 لملفات checked ونموذج المحرك لـ Unicorn البرمجي. تعتمد المطابقة على عرض المعامل ووحدة الحجز المادية.
+
+يملك `AArch64AtomicInstructions.def` قواعد قبول LSE، ويملك `AArch64AtomicExecution` الإكمال الذري. يشترك `AArch64AtomicMemory` مع العمليات الحصرية في المحاذاة والأخطاء ذات الأنواع؛ وتستخدم checked وجسر Unicorn البرمجي هذه الجهات المشتركة.
 
 تتحقق `objcNonEscapingBlockSourceFrameEffects` من الاستعارة المتزامنة لكتل المكدس باستخدام الاستعلام المشترك `sourceFrameCallArgumentStorage`. تعيد فحص التعليمات الأصلية والإرسال المؤهل الحالي والاستيراد القوي والترويسة والواصف وABI للاستدعاء وحقائق البايتات الواصلة. يحدد الواصف نطاقًا قابلًا للكتابة؛ لا تصبح بايتات الحشو مهيأة، وتبقى أنواع الحقول وأجسام الاستدعاء بحاجة إلى إثبات مستقل. تُرفض الملاحظات الدورية والتقاط مؤشرات الإطار الخاص، وتستخدم الاعتماديات جولات إثبات مكتملة.
 

docs/ar/cpu-execution.md

@@ -204,4 +204,7 @@ neverd cpu-capabilities \
 
 [Setup, signing and native hardware validation (English)](../macos-hvf.md)
 
-يدعم ARM64 checked تعليمات `LDXR/STXR` بعرض 8/16/32/64 بت، وأزواج `LDXP/STXP` بعرض 32/64 بت، وصيغ acquire/release و`CLREX`. تشترك KVM وWHP وUnicorn checked في مراقب على مستوى ISA يتتبع حجوزات مادية بحجم 16 بايت؛ ولا تمنع مخارج التنفيذ خطوة بخطوة تقدّم الحلقات. تُبطل الكتابات المعتمدة الحجز حتى إن بقيت البايتات كما هي، بما يشمل الأسماء البديلة والعروض المحتفظ بها. يحفظ الإيقاف الحالة غير المنشورة، ولا تلغي اللقطات الكتابات اللاحقة. تتبع العمليات الحصرية checked قواعد FEAT_LSE2: يُسمح بالمعامل غير المحاذى داخل كتلة محاذاة بحجم 16 بايت، ويؤدي عبور حدودها إلى `alignment`. تُطابق الكتابات ذات العرض نفسه وحدة الحجز المادية. تُفحص المحاذاة والصلاحيات قبل تقرير نجاح التخزين المشروط حتى عند انتهاء الحجز. لا يشمل هذا الملف MMIO أو تعليمات LSE الذرية الاختيارية أو SMP المتوازي. يستخدم Unicorn ARM64 هذا المراقب أيضًا ضمن عقد `Software`، بما في ذلك مشاركة RAM المادية بين وحدات CPU البرمجية ووحدات checked. يحتفظ عقد `Software` في Unicorn بنموذج المحاذاة الطبيعية للمحرك.
+يدعم ARM64 checked تعليمات `LDXR/STXR` بعرض 8/16/32/64 بت، وأزواج `LDXP/STXP` بعرض 32/64 بت، وصيغ acquire/release و`CLREX`. تشترك KVM وWHP وUnicorn checked في مراقب على مستوى ISA يتتبع حجوزات مادية بحجم 16 بايت؛ ولا تمنع مخارج التنفيذ خطوة بخطوة تقدّم الحلقات. تُبطل الكتابات المعتمدة الحجز حتى إن بقيت البايتات كما هي، بما يشمل الأسماء البديلة والعروض المحتفظ بها. يحفظ الإيقاف الحالة غير المنشورة، ولا تلغي اللقطات الكتابات اللاحقة. تتبع العمليات الحصرية checked قواعد FEAT_LSE2: يُسمح بالمعامل غير المحاذى داخل كتلة محاذاة بحجم 16 بايت، ويؤدي عبور حدودها إلى `alignment`. تُطابق الكتابات ذات العرض نفسه وحدة الحجز المادية. تُفحص المحاذاة والصلاحيات قبل تقرير نجاح التخزين المشروط حتى عند انتهاء الحجز. لا يشمل هذا الملف MMIO أو SMP المتوازي. يستخدم Unicorn ARM64 هذا المراقب أيضًا ضمن عقد `Software`، بما في ذلك مشاركة RAM المادية بين وحدات CPU البرمجية ووحدات checked. يحتفظ عقد `Software` في Unicorn بنموذج المحاذاة الطبيعية للمحرك.
+
+
+تدعم طبقة ISA المشتركة FEAT_LSE: ‏`CAS/CASP` و`SWP` و`LDADD/LDCLR/LDEOR/LDSET` وmin/max الموقعة وغير الموقعة، بعرض بايت ونصف كلمة وكلمة وكلمة مزدوجة، مع صيغ acquire/release. تتبع checked المحاذاة المذكورة أعلاه، بينما يحتفظ Unicorn `Software` بالمحاذاة الطبيعية. تراعي المقارنات عرض المعامل وتُوسّع القيم القديمة المعادة بأصفار. يتطلب CAS الفاشل إذن الكتابة أيضًا ويعيد كتابة القيمة القديمة، وهو خيار تسمح به Arm ويبطل الحجوزات المادية. ترى callbacks حالة CPU/RAM السابقة؛ ولا تنشر الإلغاءات والأخطاء المتزامنة آثارًا جزئية. يرتب قفل التنفيذ المادي وحدات CPU التعاونية دون توفير SMP متوازٍ أو عمليات MMIO ذرية. تنقل `MRS/MSR NZCV` أعلام الشرط الأربعة وفق قواعد البتات المحجوزة والسجل الصفري. تُفحص صلاحية القراءة أولًا: يؤدي المعامل غير القابل للقراءة إلى خطأ قراءة، والمعامل المخصص للقراءة فقط إلى خطأ كتابة، وفقًا للمشاهدات الأصلية على Windows ARM64.

docs/ar/testing.md

@@ -1438,6 +1438,8 @@ build-release/bin/NeverDByteCellScalarizationTests
 يغطي `AArch64ExclusiveTests.cpp` العروض والأزواج وصيغ acquire/release وتداخل السجلات والأسماء البديلة والأخطاء واللقطات وإلغاء المراقبين أو فشلهم وتنافس وحدات CPU. ويغطي `RAMReservationTests.cpp` الكتابات المتطابقة وABA وإعادة التخصيص والتراجع وتأثير تعليمات السلاسل و`ENTER` في KVM/Unicorn. تنفذ عينات عمليات Windows ARM64 الأصلية حلقات حصرية. يشغّل `scripts/check_aarch64_exclusives.py` التعليمات الأصلية ويسجل استثناءات المحاذاة في Windows ARM64 CI. لا تثبت هذه المشاهدات تنفيذ خلفيات ARM64 KVM/WHP؛ وتبقى الملفات غير المتاحة مسجلة بوضوح كتغطية متجاوزة. تغطي الحالات نفسها Unicorn البرمجي والتداخل بين العقود والكتابات المتطابقة وABA والأسماء البديلة القابلة للتنفيذ ضمن التشغيل نفسه، إضافة إلى `DC ZVA` والإلغاء بواسطة المراقبين.
  يشغّل `windows-alignment-oracle.yml` مسبار ARM64 أيضًا: تغطي 1,320 مشاهدة كل إزاحة غير محاذاة وأربعة تسلسلات تحميل وتخزين وذاكرة قابلة للكتابة أو للقراءة فقط أو محظورة أو عابرة لحدود الصفحات. يحتفظ المسبار بعرض قيم السجلات الابتدائية كاملًا ويسجل أي كتابة جزئية معتمدة قبل الخطأ. يقارن `WindowsExclusiveProcessTests.cpp` عدد 1,320 مشاهدة أصلية لـ Windows ARM64 بالبصمات الأصلية في `WindowsExclusiveNative.def`. يطبّع مواضع الشفرة والبيانات فقط، مع إبقاء قيم السجلات وبيانات الاستثناءات وتأثيرات RAM.
 
+يغطي `AArch64AtomicTests.cpp` عدد 168 ترميزًا مستقل التجميع لتعليمات LSE، وتداخل السجلات والمقارنات الموقعة والصلاحيات والإلغاء والحجوزات المادية ونقل NZCV. يجمع `scripts/check_aarch64_atomics.py` عدد 1,100 سجل أصلي من Windows ARM64 يتضمن النتائج وسياق الاستثناء ونطاق RAM كاملًا؛ وترفض اختبارات المحلل الأدلة الناقصة أو غير المتسقة. يظل تنفيذ KVM/WHP الأصلي بحاجة إلى تحقق مستقل. ينفذ `WindowsAtomicProcessTests.cpp` اختبار تراجع العملية checked، ويحفظ `WindowsAtomicResults.def` بصمات السجلات الكاملة.
+
 تستخدم الأهداف الأصلية الثابتة بنيويًا آلية الجدولة الحالية مع التحقق من إمكانية التنفيذ مباشرة. ولا يحتفظ الهدف الرمزي الوحيد بالمحمول الوارد إلا بعد تعداد شامل. تتحقق اختبارات الانحدار من 128 انتقالًا ثابتًا ضمن ميزانية استعلامات التنفيذ الخطي، ومن 32 انتقالًا محسوبًا باستعلامي تعداد لكل انتقال، مع الحفاظ على بتات العنوان العليا الحرة ومجالات الفروع. تُرفض تغييرات الحالة الكاملة وغياب المحاذاة وحدّ الأهداف الصفري وميزانيات الاستعلامات أو التعليمات غير الكافية. تظل فحوص رفض الأهداف المتعددة والتعداد غير المكتمل مطلوبة.
 
 يحتفظ الفرع الأصلي بالمجال الوارد على حافة واحدة فقط بعد اكتمال إثبات UNSAT الذي يستبعد الحافة الأخرى. تتحقق الاختبارات من 32 انتقالًا شرطيًا في كلا الاتجاهين ضمن 512 بوابة للمحلّل، ومن ميزانيات الاستعلام الدقيقة والناقصة باستعلام واحد ونفاد البوابات. يجب رفض المحاذاة المعدّلة أو المفقودة والمقارنات المعكوسة والحالة النهائية المعدّلة؛ وتظل اختبارات التحكم غير المعرّف الاعتباطي وإمكانية تنفيذ كلتا الحافتين مطلوبة.