Merge branch 'main' into client_tracing

achamayou · Oct 30, 2023 · 721a7f2 · 721a7f2
2 parents a6d5947 + af21407
commit 721a7f2
Show file tree

Hide file tree

Showing 98 changed files with 2,819 additions and 989 deletions.
diff --git a/.azure-pipelines-gh-pages.yml b/.azure-pipelines-gh-pages.yml
@@ -11,7 +11,7 @@ jobs:
     variables:
       Codeql.SkipTaskAutoInjection: true
       skipComponentGovernanceDetection: true
-    container: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15
+    container: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15
     pool:
       vmImage: ubuntu-20.04
 

diff --git a/.azure-pipelines-templates/build_check.yml b/.azure-pipelines-templates/build_check.yml
@@ -0,0 +1,4 @@
+steps:
+  - script: python3 ../scripts/build-check.py < build.log ${{ parameters.target }}
+    displayName: "Build check"
+    workingDirectory: build
diff --git a/.azure-pipelines-templates/common.yml b/.azure-pipelines-templates/common.yml
@@ -34,6 +34,11 @@ jobs:
             parameters:
               ninja_targets: "${{ parameters.ninja_targets }}"
 
+          - ${{ if and(eq(parameters.suffix, 'Release'), eq(parameters.target, 'SNPCC')) }}:
+              - template: build_check.yml
+                parameters:
+                  target: "${{ parameters.target }}"
+
           - ${{ if not(and(eq(parameters.suffix, 'Release'), eq(parameters.target, 'SNPCC'))) }}:
               - template: test.yml
                 parameters:

diff --git a/.azure-pipelines-templates/configure.yml b/.azure-pipelines-templates/configure.yml
@@ -10,14 +10,18 @@ jobs:
       - checkout: self
         clean: true
       - script: |
-          set -ex
           echo "Determine if any code has changed."
-          if git diff --ignore-submodules=dirty --quiet origin/${SYSTEM_PULLREQUEST_TARGETBRANCH:-origin/main} -- ':!doc' ':!*.md' ':!scripts/azure_deployment'; then
-            echo " - Documentation change only"
-            echo "##vso[task.setvariable variable=docOnly;isOutput=true]true" #set variable docOnly to true
-          else
-            echo " - Source has changed"
-            echo "##vso[task.setvariable variable=docOnly;isOutput=true]false" #set variable docOnly to false
+          echo "Assuming full build should be run."
+          echo "##vso[task.setvariable variable=docOnly;isOutput=true]false"
+          if [ ${SYSTEM_PULLREQUEST_TARGETBRANCH} ]; then
+            echo " - Running on PR, checking diff for non-doc changes"
+            if git diff --ignore-submodules=dirty --quiet "origin/${SYSTEM_PULLREQUEST_TARGETBRANCH}" -- ':!doc' ':!*.md' ':!scripts/azure_deployment'; then
+              echo " - Documentation change only"
+              echo "##vso[task.setvariable variable=docOnly;isOutput=true]true"
+            else
+              echo " - Source has changed"
+            fi
           fi
+
         displayName: "Check for runtime changes"
         name: setVarStep
diff --git a/.azure-pipelines-templates/deploy_aci.yml b/.azure-pipelines-templates/deploy_aci.yml
@@ -60,7 +60,7 @@ jobs:
           ACR_TOKEN_NAME: ci-push-token
           ACR_CI_PUSH_TOKEN_PASSWORD: $(ACR_CI_PUSH_TOKEN_PASSWORD)
           ACR_REGISTRY: ccfmsrc.azurecr.io
-          BASE_IMAGE: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-snp-clang15
+          BASE_IMAGE: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-snp-clang15
 
       - script: |
           set -ex

diff --git a/.azure-pipelines-templates/ninja.yml b/.azure-pipelines-templates/ninja.yml
@@ -1,4 +1,6 @@
 steps:
-  - script: ninja ${{ parameters.ninja_targets }}
+  - script: |
+      set -ex
+      ninja -v ${{ parameters.ninja_targets }} | tee build.log
     displayName: Ninja
     workingDirectory: build
diff --git a/.azure-pipelines-templates/release.yml b/.azure-pipelines-templates/release.yml
@@ -14,7 +14,7 @@ jobs:
 
       - script: |
           set -ex
-          python3.8 ./scripts/extract-release-notes.py --target-git-version --append-mcr-images | tee $(Build.BinariesDirectory)/rel-notes.md
+          python3.8 ./scripts/extract-release-notes.py --target-git-version --append-mcr-images --describe-path-changes "./samples/constitution" | tee $(Build.BinariesDirectory)/rel-notes.md
         displayName: Extract release notes
 
       - script: |

diff --git a/.azure-pipelines-templates/trace_validation.yml b/.azure-pipelines-templates/trace_validation.yml
@@ -9,7 +9,7 @@ steps:
   - script: |
       set -ex
       cd tla/
-      parallel 'JSON={} ./tlc.sh Traceccfraft.tla' ::: \
+      parallel 'JSON={} ./tlc.sh consensus/Traceccfraft.tla' ::: \
       ../build/replicate.ndjson \
       ../build/election.ndjson \
       ../build/multi_election.ndjson \

diff --git a/.azure-pipelines.yml b/.azure-pipelines.yml
@@ -29,15 +29,15 @@ schedules:
 resources:
   containers:
     - container: virtual
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15
       options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro
 
     - container: snp
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-snp-clang15
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-snp-clang15
       options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro
 
     - container: sgx
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-sgx
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-sgx
       options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --device /dev/sgx_enclave:/dev/sgx_enclave --device /dev/sgx_provision:/dev/sgx_provision -v /dev/sgx:/dev/sgx -v /lib/modules:/lib/modules:ro
 
 variables:

diff --git a/.azure_pipelines_snp.yml b/.azure_pipelines_snp.yml
@@ -30,7 +30,7 @@ schedules:
 resources:
   containers:
     - container: virtual
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15
       options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro
 
 jobs:

diff --git a/.daily.yml b/.daily.yml
@@ -25,15 +25,15 @@ schedules:
 resources:
   containers:
     - container: virtual
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15
       options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE
 
     - container: snp
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-snp-clang15
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-snp-clang15
       options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro
 
     - container: sgx
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-sgx
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-sgx
       options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --device /dev/sgx_enclave:/dev/sgx_enclave --device /dev/sgx_provision:/dev/sgx_provision -v /dev/sgx:/dev/sgx
 
 jobs:

diff --git a/.daily_canary b/.daily_canary
@@ -1,4 +1,4 @@
    -^-     ___           ___
   (- -)   (= =)   |     Y   &  +--?
  (  V  ) /  .  \  |    +---=---'
-/--x-m- /--n-n---xXx--/--yY------>>>----<<<
+/--x-m- /--n-n---xXx--/--yY------>>>----<<<>>]]{{}}
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
@@ -1,6 +1,6 @@
 {
   "name": "CCF Development Environment",
-  "image": "ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15",
+  "image": "ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15",
   "runArgs": [],
   "extensions": [
     "eamodio.gitlens",

diff --git a/.github/workflows/ci-checks.yml b/.github/workflows/ci-checks.yml
@@ -9,7 +9,7 @@ on:
 jobs:
   checks:
     runs-on: ubuntu-latest
-    container: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15
+    container: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15
 
     steps:
       - run: git config --global --add safe.directory "$GITHUB_WORKSPACE"

diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml
@@ -10,11 +10,11 @@ on:
   workflow_dispatch:
 
 jobs:
-  model-checking:
-    name: Model Checking
+  model-checking-consensus:
+    name: Model Checking - Consensus
     runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
     container:
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15
 
     steps:
       - uses: actions/checkout@v3
@@ -26,24 +26,26 @@ jobs:
       - name: MCccfraft.cfg
         run: |
           cd tla/
-          ./tlc.sh -workers auto MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json
+          ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json
 
       - name: MCccfraftWithReconfig.cfg
         run: |
           cd tla/
-          ./tlc.sh -workers auto -config MCccfraftWithReconfig.cfg MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
+          ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
 
       - name: Upload traces in TLA and JSON format
         uses: actions/upload-artifact@v3
         if: ${{ failure() }}
         with:
           name: tlc
           path: |
+            tla/consensus/*_TTrace_*.tla
+            tla/consensus/*_TTrace_*.bin
             tla/*.trace.tla
             tla/*.json
 
-  simulation:
-    name: Simulation
+  simulation-consensus:
+    name: Simulation - Consensus
     runs-on: ubuntu-latest
 
     steps:
@@ -53,13 +55,112 @@ jobs:
       - name: SIMccfraft.tla
         run: |
           cd tla/
-          ./tlc.sh -workers auto -simulate -depth 500 SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
+          ./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
 
       - name: Upload traces in TLA and JSON format
         uses: actions/upload-artifact@v3
         if: ${{ failure() }}
         with:
           name: tlc
           path: |
+            tla/consensus/*_TTrace_*.tla
+            tla/consensus/*_TTrace_*.bin
             tla/*.trace.tla
             tla/*.json
+
+  model-checking-consistency:
+    name: Model Checking - Consistency
+    runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
+    container:
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15
+
+    steps:
+      - uses: actions/checkout@v3
+      - run: |
+          sudo apt update
+          sudo apt install -y default-jre
+          python3 ./tla/install_deps.py
+
+      - name: consistency/MCSingleNode.cfg
+        run: |
+          cd tla/
+          ./tlc.sh -workers auto consistency/MCSingleNode.tla -dumpTrace json MCSingleNode.json
+
+      - name: consistency/MCSingleNodeReads.cfg
+        run: |
+          cd tla/
+          ./tlc.sh -workers auto consistency/MCSingleNodeReads.tla -dumpTrace json MCSingleNodeReads.json
+
+      - name: consistency/MCMultiNode.cfg
+        run: |
+          cd tla/
+          ./tlc.sh -workers auto consistency/MCMultiNode.tla -dumpTrace json MCMultiNode.json
+
+      - name: consistency/MCMultiNodeReads.cfg
+        run: |
+          cd tla/
+          ./tlc.sh -workers auto consistency/MCMultiNodeReads.tla -dumpTrace json MCMultiNodeReads.json
+
+      - name: consistency/MCMultiNodeReadsAlt.cfg
+        run: |
+          cd tla/
+          ./tlc.sh -workers auto consistency/MCMultiNodeReadsAlt.tla -dumpTrace json MCMultiNodeReadsAlt.json
+
+      - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
+        uses: actions/upload-artifact@v3
+        if: ${{ failure() }}
+        with:
+          name: tlc
+          path: |
+            tla/consistency/*_TTrace_*.tla
+            tla/*.json
+
+  counterexamples-consistency:
+    name: Counterexamples - Consistency
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v3
+      - run: python3 ./tla/install_deps.py
+
+      - name: consistency/MCSingleNodeCommitReachability.cfg
+        run: |
+          cd tla/
+          ./tlc_debug.sh -workers auto -config consistency/MCSingleNodeCommitReachability.cfg consistency/MCSingleNodeReads.tla
+
+      - name: consistency/MCMultiNodeCommitReachability.cfg
+        run: |
+          cd tla/
+          ./tlc_debug.sh -workers auto -config consistency/MCMultiNodeCommitReachability.cfg consistency/MCMultiNodeReads.tla
+
+      - name: consistency/MCMultiNodeInvalidReachability.cfg
+        run: |
+          cd tla/
+          ./tlc_debug.sh -workers auto -config consistency/MCMultiNodeInvalidReachability.cfg consistency/MCMultiNodeReads.tla
+
+      - name: consistency/MCMultiNodeReadsNotLinearizable.cfg
+        run: |
+          cd tla/
+          ./tlc_debug.sh -workers auto -config consistency/MCMultiNodeReadsNotLinearizable.cfg consistency/MCMultiNodeReads.tla
+
+  simulation-consistency:
+    name: Simulation - Consistency
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v3
+      - run: python3 ./tla/install_deps.py
+
+      - name: consistency/MultiNodeReads.cfg
+        run: |
+          cd tla/
+          ./tlc.sh -workers auto -simulate num=5 -depth 50 consistency/MultiNodeReads.tla -dumpTrace json MultiNodeReads.json
+
+      - name: Upload traces in TLA and JSON format
+        uses: actions/upload-artifact@v3
+        if: ${{ failure() }}
+        with:
+          name: tlc
+          path: |
+            tla/consistency/*_TTrace_*.tla
+            tla/*.json
diff --git a/.multi-thread.yml b/.multi-thread.yml
@@ -16,7 +16,7 @@ pr:
 resources:
   containers:
     - container: virtual
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15
       options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro
 
 jobs:

diff --git a/.snpcc_canary b/.snpcc_canary
@@ -1,4 +1,4 @@
   ___         ___    ___
- (. =)     Y (0 0)  (* *)    Y
+ (. =)     Y (0 0)  (x X)    Y
    O     \     o      |    /
 /-xXx--//-----x=x--/-xXx--/---x---->>
diff --git a/.stress.yml b/.stress.yml
@@ -20,7 +20,7 @@ schedules:
 resources:
   containers:
     - container: sgx
-      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-sgx
+      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-sgx
       options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --device /dev/sgx_enclave:/dev/sgx_enclave --device /dev/sgx_provision:/dev/sgx_provision -v /dev/sgx:/dev/sgx
 
 jobs:

diff --git a/CCF-PAPER-VLDB-2023.pdf b/CCF-PAPER-VLDB-2023.pdf
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -5,6 +5,14 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
 and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
 
+## [5.0.0-dev5]
+
+[5.0.0-dev5]: https://github.com/microsoft/CCF/releases/tag/ccf-5.0.0-dev5
+
+- In governance contexts, JS runtimes now only use runtime limits from the [public:ccf.gov.js_runtime_options map](https://microsoft.github.io/CCF/main/audit/builtin_maps.html#js-runtime-options) if they are strictly higher than the defaults (#5730).
+- Fixed an issue where a JS runtime limit could be hit out of user code execution, leading to an incorrectly constructed JS runtime or a crash (#5730).
+- Added a GET /node/primary endpoint, returning 200 when primary and 404 when not, for load balancers to use (#5789).
+
 ## [5.0.0-dev4]
 
 [5.0.0-dev4]: https://github.com/microsoft/CCF/releases/tag/ccf-5.0.0-dev4

diff --git a/doc/architecture/index.rst b/doc/architecture/index.rst
@@ -48,7 +48,7 @@ Architecture
     :fa:`check-double` :doc:`raft_tla`
     ^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-    A TLA+ model of Raft as modified when implemented in CCF.
+    TLA+ specifications of CCF.
 
     ---