From 1988bd62dc7d2c051d707783c362c1063e62b497 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sat, 10 Feb 2024 12:43:31 +1100
Subject: [PATCH 01/11] workflows: factor out common seL4 workflows

These can now be called from other workflows, reducing duplication.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/pr.yml           |   8 +-
 .github/workflows/push.yml         |   7 +-
 .github/workflows/sel4bench-pr.yml | 123 +++++++++++++++++++++++++++++
 .github/workflows/sel4test-hw.yml  | 116 +++++++++++++++++++++++++++
 .github/workflows/sel4test-sim.yml |  35 ++++++++
 5 files changed, 282 insertions(+), 7 deletions(-)
 create mode 100644 .github/workflows/sel4bench-pr.yml
 create mode 100644 .github/workflows/sel4test-hw.yml
 create mode 100644 .github/workflows/sel4test-sim.yml

diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml
index c0f53980..2291ece0 100644
--- a/.github/workflows/pr.yml
+++ b/.github/workflows/pr.yml
@@ -6,7 +6,7 @@
 
 name: PR
 
-on: [pull_request]
+on: [pull_request, workflow_call]
 
 jobs:
   gitlint:
@@ -26,3 +26,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - uses: seL4/ci-actions/bashisms@master
+
+  style:
+    name: Style
+    runs-on: ubuntu-latest
+    steps:
+    - uses: seL4/ci-actions/style@master
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index f5f34368..9388e929 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -10,6 +10,7 @@ on:
     branches:
       - master
   pull_request:
+  workflow_call:
 
 jobs:
   check:
@@ -25,9 +26,3 @@ jobs:
       - uses: seL4/ci-actions/link-check@master
         with:
           exclude: '/node_modules/'
-
-  style:
-    name: Style
-    runs-on: ubuntu-latest
-    steps:
-    - uses: seL4/ci-actions/style@master
diff --git a/.github/workflows/sel4bench-pr.yml b/.github/workflows/sel4bench-pr.yml
new file mode 100644
index 00000000..a986d096
--- /dev/null
+++ b/.github/workflows/sel4bench-pr.yml
@@ -0,0 +1,123 @@
+# Copyright 2022, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+# Build and run sel4bench on pull requests, on label request
+
+name: seL4Bench-HW
+
+on:
+  workflow_call:
+
+# intended to run on
+#  pull_request_target:
+#    types: [opened, reopened, synchronize, labeled]
+
+# downgrade permissions to read-only as you would have in a standard PR action
+permissions:
+  contents: read
+
+# To reduce the load (especiually on the machine queue) we cancel any older runs
+# of this workflow for the current PR. Such runs exist, if there were new pushes
+# to the PR's branch without waiting for the workflow to finish. As a side
+# effect, pushing new commits now becomes a convenient way to cancel all the
+# older runs, e.g. if they are stuck and would only be stopped by the timeout
+# eventually.
+# Note that we could do the concurrency handling at a finer level, and only wrap
+# the actual run on the hardware. But there seems not much gain in letting the
+# older builds run, as these are usually obsolete with new pushes also.
+concurrency:
+  group: ${{ github.workflow }}-pr-${{ github.event.number }}
+  cancel-in-progress: true
+
+jobs:
+  code:
+    name: Freeze Code
+    runs-on: ubuntu-latest
+    if: ${{ github.event_name == 'pull_request_target' &&
+               github.event.action != 'labeled' &&
+               contains(github.event.pull_request.labels.*.name, 'hw-bench') ||
+            github.event_name == 'pull_request_target' &&
+               github.event.action == 'labeled' &&
+               github.event.label.name == 'hw-bench' }}
+    outputs:
+      xml: ${{ steps.repo.outputs.xml }}
+    steps:
+    - id: repo
+      uses: seL4/ci-actions/repo-checkout@master
+      with:
+        manifest_repo: sel4bench-manifest
+        manifest: master.xml
+        sha: ${{ github.event.pull_request.head.sha }}
+
+  build:
+    name: Build
+    needs: code
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        march: [armv7a, armv8a, nehalem, rv64imac]
+    steps:
+    - name: Build
+      uses: seL4/ci-actions/sel4bench@master
+      with:
+        xml: ${{ needs.code.outputs.xml }}
+        march: ${{ matrix.march }}
+    - name: Upload images
+      uses: actions/upload-artifact@v4
+      with:
+        name: images-${{ matrix.march }}
+        path: '*-images.tar.gz'
+
+  hw-run:
+    name: HW Benchmark
+    if: ${{ github.repository_owner == 'seL4' }}
+    runs-on: ubuntu-latest
+    needs: [build]
+    strategy:
+      fail-fast: false
+      matrix:
+        platform:
+          - sabre
+          - imx8mm_evk
+          - odroid_c2
+          - odroid_xu4
+          - am335x_boneblack
+          - tx1
+          - tx2
+          - hifive
+        include:
+          - platform: pc99
+            req: skylake
+          - platform: pc99
+            req: haswell3
+    steps:
+      - name: Get machine queue
+        uses: actions/checkout@v4
+        with:
+          repository: seL4/machine_queue
+          path: machine_queue
+      - name: Get march
+        id: plat
+        uses: seL4/ci-actions/march-of-platform@master
+        with:
+          platform: ${{ matrix.platform }}
+      - name: Download image
+        uses: actions/download-artifact@v4
+        with:
+          name: images-${{ steps.plat.outputs.march }}
+      - name: Run
+        uses: seL4/ci-actions/sel4bench-hw@master
+        with:
+          platform: ${{ matrix.platform }}
+          req: ${{ matrix.req }}
+          index: $${{ strategy.job-index }}
+        env:
+          HW_SSH: ${{ secrets.HW_SSH }}
+      - name: Upload results
+        uses: actions/upload-artifact@v4
+        with:
+          # funky expression below is to work around lack of ternary operator
+          name: sel4bench-results-${{ matrix.platform }}${{ matrix.req != '' && format('-{0}', matrix.req) || '' }}
+          path: '*.json'
diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml
new file mode 100644
index 00000000..1a9f21b1
--- /dev/null
+++ b/.github/workflows/sel4test-hw.yml
@@ -0,0 +1,116 @@
+# Copyright 2021, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+# sel4test hardware builds and runs
+#
+# See sel4test-hw/builds.yml in the repo seL4/ci-actions for configs.
+
+name: seL4Test-HW
+
+on:
+  workflow_call:
+
+# intended to run on
+#  pull_request_target:
+#    types: [opened, reopened, synchronize, labeled]
+# needs PR target for secrets access; guard by requiring label
+
+# downgrade permissions to read-only as you would have in a standard PR action
+permissions:
+  contents: read
+
+# To reduce the load (especiually on the machine queue) we cancel any older runs
+# of this workflow for the current PR. Such runs exist, if there were new pushes
+# to the PR's branch without waiting for the workflow to finish. As a side
+# effect, pushing new commits now becomes a convenient way to cancel all the
+# older runs, e.g. if they are stuck and would only be stopped by the timeout
+# eventually.
+# Note that we could do the concurrency handling at a finer level, and only wrap
+# the actual run on the hardware. But there seems not much gain in letting the
+# older builds run, as these are usually obsolete with new pushes also.
+concurrency:
+  group: ${{ github.workflow }}-pr-${{ github.event.number }}
+  cancel-in-progress: true
+
+jobs:
+  hw-build:
+    name: HW Build
+    runs-on: ubuntu-latest
+    if: ${{ github.event_name == 'push' ||
+            github.event_name == 'pull_request_target' &&
+              github.event.action != 'labeled' &&
+              (contains(github.event.pull_request.labels.*.name, 'hw-build') ||
+               contains(github.event.pull_request.labels.*.name, 'hw-test')) ||
+            github.event_name == 'pull_request_target' &&
+              github.event.action == 'labeled' &&
+              (github.event.label.name == 'hw-build' ||
+               github.event.label.name == 'hw-test') }}
+    strategy:
+      fail-fast: false
+      matrix:
+        # There is no "rv32imac" hardware yet.
+        march: [armv7a, armv8a, nehalem, rv64imac]
+        compiler: [gcc, clang]
+    steps:
+    - name: Build
+      uses: seL4/ci-actions/sel4test-hw@master
+      with:
+        march: ${{ matrix.march }}
+        compiler: ${{ matrix.compiler }}
+        sha: ${{ github.event.pull_request.head.sha }}
+    - name: Upload images
+      uses: actions/upload-artifact@v4
+      with:
+        name: images-${{ matrix.march }}-${{ matrix.compiler }}
+        path: '*-images.tar.gz'
+    - name: Upload kernel.elf files
+      uses: actions/upload-artifact@v4
+      with:
+        name: kernel.elf-${{ matrix.march }}-${{ matrix.compiler }}
+        path: '*-kernel.elf'
+
+  the_matrix:
+    name: Matrix
+    needs: hw-build
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.matrix.outputs.matrix }}
+    steps:
+    - id: matrix
+      uses: seL4/ci-actions/sel4test-hw-matrix@master
+
+  hw-run:
+    name: HW Run
+    runs-on: ubuntu-latest
+    needs: the_matrix
+    if: ${{ github.repository_owner == 'seL4' &&
+            (github.event_name == 'push' ||
+             github.event_name == 'pull_request_target' &&
+               github.event.action != 'labeled' &&
+               contains(github.event.pull_request.labels.*.name, 'hw-test') ||
+             github.event_name == 'pull_request_target' &&
+               github.event.action == 'labeled' &&
+               github.event.label.name == 'hw-test') }}
+    strategy:
+      fail-fast: false
+      matrix: ${{ fromJson(needs.the_matrix.outputs.matrix) }}
+    steps:
+      - name: Get machine queue
+        uses: actions/checkout@v4
+        with:
+          repository: seL4/machine_queue
+          path: machine_queue
+      - name: Download image
+        uses: actions/download-artifact@v4
+        with:
+          name: images-${{ matrix.march }}-${{ matrix.compiler }}
+      - name: Run
+        uses: seL4/ci-actions/sel4test-hw-run@master
+        with:
+          platform: ${{ matrix.platform }}
+          compiler: ${{ matrix.compiler }}
+          mode: ${{ matrix.mode }}
+          index: $${{ strategy.job-index }}
+        env:
+          HW_SSH: ${{ secrets.HW_SSH }}
diff --git a/.github/workflows/sel4test-sim.yml b/.github/workflows/sel4test-sim.yml
new file mode 100644
index 00000000..3986adc6
--- /dev/null
+++ b/.github/workflows/sel4test-sim.yml
@@ -0,0 +1,35 @@
+# Copyright 2021, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+# sel4test simulation runs
+#
+# See sel4test-sim/builds.yml in the repo seL4/ci-actions for configs.
+
+name: seL4Test-Sim
+
+on:
+  workflow_call:
+
+# To reduce the load we cancel any older runs of this workflow for the current
+# PR. Such runs exist, if there were new pushes to the PR's branch without
+# waiting for the workflow to finish. As a side effect, pushing new commits now
+# becomes a convenient way to cancel all the older runs, e.g. if they are stuck
+# and would only be stopped by the timeout eventually.
+concurrency:
+  group: ${{ github.workflow }}-pr-${{ github.event.number }}
+  cancel-in-progress: true
+
+jobs:
+  sim:
+    name: Simulation
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        march: [armv7a, armv8a, nehalem, rv32imac, rv64imac]
+        compiler: [gcc, clang]
+    steps:
+    - uses: seL4/ci-actions/sel4test-sim@master
+      with:
+        march: ${{ matrix.march }}
+        compiler: ${{ matrix.compiler }}

From cd0ecc0c07c588b2d6a273213d53bb28ea3e6374 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sat, 10 Feb 2024 13:57:51 +1100
Subject: [PATCH 02/11] workflows: use job concurrency groups

- use job concurrency instead of workflow concurrency, because on the
  workflow level a label trigger event will already call all current
  runs, whereas the job level is guarded by `if` conditions.

- disambiguate concurrency group names, because the workflow name is
  inherited from the caller.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/sel4bench-pr.yml | 21 ++++++++-------------
 .github/workflows/sel4test-hw.yml  | 21 ++++++++-------------
 .github/workflows/sel4test-sim.yml |  8 +++-----
 3 files changed, 19 insertions(+), 31 deletions(-)

diff --git a/.github/workflows/sel4bench-pr.yml b/.github/workflows/sel4bench-pr.yml
index a986d096..5b282d0e 100644
--- a/.github/workflows/sel4bench-pr.yml
+++ b/.github/workflows/sel4bench-pr.yml
@@ -17,19 +17,6 @@ on:
 permissions:
   contents: read
 
-# To reduce the load (especiually on the machine queue) we cancel any older runs
-# of this workflow for the current PR. Such runs exist, if there were new pushes
-# to the PR's branch without waiting for the workflow to finish. As a side
-# effect, pushing new commits now becomes a convenient way to cancel all the
-# older runs, e.g. if they are stuck and would only be stopped by the timeout
-# eventually.
-# Note that we could do the concurrency handling at a finer level, and only wrap
-# the actual run on the hardware. But there seems not much gain in letting the
-# older builds run, as these are usually obsolete with new pushes also.
-concurrency:
-  group: ${{ github.workflow }}-pr-${{ github.event.number }}
-  cancel-in-progress: true
-
 jobs:
   code:
     name: Freeze Code
@@ -54,6 +41,11 @@ jobs:
     name: Build
     needs: code
     runs-on: ubuntu-latest
+    # To reduce the load on GitHub runner numbers and machine queue we cancel
+    # any older runs of this workflow for the current PR.
+    concurrency:
+      group: ${{ github.workflow }}-sel4bench-pr-build-${{ github.event.number }}
+      cancel-in-progress: true
     strategy:
       fail-fast: false
       matrix:
@@ -75,6 +67,9 @@ jobs:
     if: ${{ github.repository_owner == 'seL4' }}
     runs-on: ubuntu-latest
     needs: [build]
+    concurrency:
+      group: ${{ github.workflow }}-sel4bench-pr-hw-run-${{ github.event.number }}
+      cancel-in-progress: true
     strategy:
       fail-fast: false
       matrix:
diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml
index 1a9f21b1..9a66d82c 100644
--- a/.github/workflows/sel4test-hw.yml
+++ b/.github/workflows/sel4test-hw.yml
@@ -20,19 +20,6 @@ on:
 permissions:
   contents: read
 
-# To reduce the load (especiually on the machine queue) we cancel any older runs
-# of this workflow for the current PR. Such runs exist, if there were new pushes
-# to the PR's branch without waiting for the workflow to finish. As a side
-# effect, pushing new commits now becomes a convenient way to cancel all the
-# older runs, e.g. if they are stuck and would only be stopped by the timeout
-# eventually.
-# Note that we could do the concurrency handling at a finer level, and only wrap
-# the actual run on the hardware. But there seems not much gain in letting the
-# older builds run, as these are usually obsolete with new pushes also.
-concurrency:
-  group: ${{ github.workflow }}-pr-${{ github.event.number }}
-  cancel-in-progress: true
-
 jobs:
   hw-build:
     name: HW Build
@@ -46,6 +33,11 @@ jobs:
               github.event.action == 'labeled' &&
               (github.event.label.name == 'hw-build' ||
                github.event.label.name == 'hw-test') }}
+    # To reduce the load (especiually on the machine queue) we cancel any older
+    # runs of this workflow for the current PR.
+    concurrency:
+      group: ${{ github.workflow }}-sel4test-pr-build-${{ github.event.number }}
+      cancel-in-progress: true
     strategy:
       fail-fast: false
       matrix:
@@ -92,6 +84,9 @@ jobs:
              github.event_name == 'pull_request_target' &&
                github.event.action == 'labeled' &&
                github.event.label.name == 'hw-test') }}
+    concurrency:
+      group: ${{ github.workflow }}-sel4test-pr-hw-run-${{ github.event.number }}
+      cancel-in-progress: true
     strategy:
       fail-fast: false
       matrix: ${{ fromJson(needs.the_matrix.outputs.matrix) }}
diff --git a/.github/workflows/sel4test-sim.yml b/.github/workflows/sel4test-sim.yml
index 3986adc6..330f45a5 100644
--- a/.github/workflows/sel4test-sim.yml
+++ b/.github/workflows/sel4test-sim.yml
@@ -12,12 +12,10 @@ on:
   workflow_call:
 
 # To reduce the load we cancel any older runs of this workflow for the current
-# PR. Such runs exist, if there were new pushes to the PR's branch without
-# waiting for the workflow to finish. As a side effect, pushing new commits now
-# becomes a convenient way to cancel all the older runs, e.g. if they are stuck
-# and would only be stopped by the timeout eventually.
+# PR. Ok on the workflow level here, because this workflow does not re-trigger
+# on "labeled" events.
 concurrency:
-  group: ${{ github.workflow }}-pr-${{ github.event.number }}
+  group: ${{ github.workflow }}-sel4sim-pr-${{ github.event.number }}
   cancel-in-progress: true
 
 jobs:

From 80f4e3d1198b08a29277a5ba446c5f9e24ff3c24 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sun, 11 Feb 2024 16:50:10 +1100
Subject: [PATCH 03/11] workflows: disallow push for sel4test-hw

The workflow is intended to only run for pull_request_target.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/sel4test-hw.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml
index 9a66d82c..ce022e50 100644
--- a/.github/workflows/sel4test-hw.yml
+++ b/.github/workflows/sel4test-hw.yml
@@ -24,8 +24,7 @@ jobs:
   hw-build:
     name: HW Build
     runs-on: ubuntu-latest
-    if: ${{ github.event_name == 'push' ||
-            github.event_name == 'pull_request_target' &&
+    if: ${{ github.event_name == 'pull_request_target' &&
               github.event.action != 'labeled' &&
               (contains(github.event.pull_request.labels.*.name, 'hw-build') ||
                contains(github.event.pull_request.labels.*.name, 'hw-test')) ||

From d2047cf87f225043c40166325c48fa9e4b6790ec Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sun, 11 Feb 2024 16:50:44 +1100
Subject: [PATCH 04/11] workflows: use Freeze Code step for sel4test-hw

This makes sure all build jobs run on the same repo manifest state.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/sel4test-hw.yml | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml
index ce022e50..686ed80d 100644
--- a/.github/workflows/sel4test-hw.yml
+++ b/.github/workflows/sel4test-hw.yml
@@ -21,8 +21,8 @@ permissions:
   contents: read
 
 jobs:
-  hw-build:
-    name: HW Build
+  code:
+    name: Freeze Code
     runs-on: ubuntu-latest
     if: ${{ github.event_name == 'pull_request_target' &&
               github.event.action != 'labeled' &&
@@ -32,7 +32,21 @@ jobs:
               github.event.action == 'labeled' &&
               (github.event.label.name == 'hw-build' ||
                github.event.label.name == 'hw-test') }}
-    # To reduce the load (especiually on the machine queue) we cancel any older
+    outputs:
+      xml: ${{ steps.repo.outputs.xml }}
+    steps:
+    - id: repo
+      uses: seL4/ci-actions/repo-checkout@master
+      with:
+        manifest_repo: sel4test-manifest
+        manifest: master.xml
+        sha: ${{ github.event.pull_request.head.sha }}
+
+  hw-build:
+    name: HW Build
+    runs-on: ubuntu-latest
+    needs: code
+    # To reduce the load (especially on the machine queue) we cancel any older
     # runs of this workflow for the current PR.
     concurrency:
       group: ${{ github.workflow }}-sel4test-pr-build-${{ github.event.number }}
@@ -47,9 +61,9 @@ jobs:
     - name: Build
       uses: seL4/ci-actions/sel4test-hw@master
       with:
+        xml: ${{ needs.code.outputs.xml }}
         march: ${{ matrix.march }}
         compiler: ${{ matrix.compiler }}
-        sha: ${{ github.event.pull_request.head.sha }}
     - name: Upload images
       uses: actions/upload-artifact@v4
       with:

From 3cd69b6b37bdf184f574e145932582eae360e3e4 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Thu, 15 Feb 2024 09:31:47 +1100
Subject: [PATCH 05/11] workflows: factor out event name guard

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/sel4test-hw.yml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml
index 686ed80d..c40f713c 100644
--- a/.github/workflows/sel4test-hw.yml
+++ b/.github/workflows/sel4test-hw.yml
@@ -25,13 +25,14 @@ jobs:
     name: Freeze Code
     runs-on: ubuntu-latest
     if: ${{ github.event_name == 'pull_request_target' &&
+            (
               github.event.action != 'labeled' &&
               (contains(github.event.pull_request.labels.*.name, 'hw-build') ||
                contains(github.event.pull_request.labels.*.name, 'hw-test')) ||
-            github.event_name == 'pull_request_target' &&
               github.event.action == 'labeled' &&
               (github.event.label.name == 'hw-build' ||
-               github.event.label.name == 'hw-test') }}
+               github.event.label.name == 'hw-test')
+            ) }}
     outputs:
       xml: ${{ steps.repo.outputs.xml }}
     steps:

From 37666b1476a9fe8186a3c0cdaa674560b6c75ced Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sat, 17 Feb 2024 12:37:12 +1100
Subject: [PATCH 06/11] label check refactor

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/sel4bench-pr.yml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/sel4bench-pr.yml b/.github/workflows/sel4bench-pr.yml
index 5b282d0e..0a0aadb9 100644
--- a/.github/workflows/sel4bench-pr.yml
+++ b/.github/workflows/sel4bench-pr.yml
@@ -22,11 +22,12 @@ jobs:
     name: Freeze Code
     runs-on: ubuntu-latest
     if: ${{ github.event_name == 'pull_request_target' &&
+            (
                github.event.action != 'labeled' &&
-               contains(github.event.pull_request.labels.*.name, 'hw-bench') ||
-            github.event_name == 'pull_request_target' &&
+                contains(github.event.pull_request.labels.*.name, 'hw-bench') ||
                github.event.action == 'labeled' &&
-               github.event.label.name == 'hw-bench' }}
+                github.event.label.name == 'hw-bench'
+            ) }}
     outputs:
       xml: ${{ steps.repo.outputs.xml }}
     steps:

From 6e1ac99d503d5e91817476aba4dd4ef0c068ec13 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sun, 11 Feb 2024 16:56:02 +1100
Subject: [PATCH 07/11] workflows: rename to sel4bench-hw for consistency

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/{sel4bench-pr.yml => sel4bench-hw.yml} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename .github/workflows/{sel4bench-pr.yml => sel4bench-hw.yml} (100%)

diff --git a/.github/workflows/sel4bench-pr.yml b/.github/workflows/sel4bench-hw.yml
similarity index 100%
rename from .github/workflows/sel4bench-pr.yml
rename to .github/workflows/sel4bench-hw.yml

From 9e5b3eca728fed4e88577c1158213f84572eff59 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sat, 10 Feb 2024 13:38:45 +1100
Subject: [PATCH 08/11] README: add descriptions of common workflows

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 README.md | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index fc638361..3bb801db 100644
--- a/README.md
+++ b/README.md
@@ -5,7 +5,7 @@
 
 [![CI](https://github.com/seL4/ci-actions/actions/workflows/push.yml/badge.svg)](https://github.com/seL4/ci-actions/actions/workflows/push.yml)
 
-# CI actions for seL4 repositories
+# CI actions and Workflows for seL4 repositories
 
 This repository collects definitions for continuous integration (CI)
 tasks/actions for the repositories of the seL4 foundation. While some of these
@@ -15,11 +15,22 @@ The idea is to concentrate most of the GitHub workflow definitions here in a
 single repository to avoid duplication, share code between actions, and to make
 it easier to replicate a similar CI setup on other platforms.
 
-Currently, everything is fairly GitHub-specific, but that could change over
-time.
-
 Shared JavaScript is in [`js/`](js/), and shared shell scripts are in [`scripts/`](scripts/)
 
+This repository also defines a number of GitHub action workflows that can be
+called from other repositories. These are all files in `.github/workflows` that
+define an `on: workflow_call` trigger. In particular:
+
+- [pr.yml](.github/workflows/pr.yml) for standard pull requests checks (gitlint,
+  whitespace, shell checks, style)
+- [push.yml](.github/workflows/push.yml) for standard push checks (links, licenses)
+- [sel4test-sim.yml](.github/workflows/sel4test-sim.yml) for running the
+  seL4 simulation tests
+- [sel4test-hw.yml](.github/workflows/sel4test-hw.yml) for running the
+  seL4 hardware tests
+- [sel4bench-hw.yml](.github/workflows/sel4bench-hw.yml) for running the
+  seL4 hardware benchmarks
+
 ## Availabe actions
 
 The following GitHub actions are available:

From 00d3a04581ca25bad6572cc069c0e0a8856d7564 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Tue, 13 Feb 2024 09:21:12 +1100
Subject: [PATCH 09/11] workflows: strategy.job-index for concurrency

Add the strategy.job-index back into the concurrency key, now that
these are back at the job level.

Co-authored-by: Axel Heider <axel-h@users.noreply.github.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/sel4bench-hw.yml | 4 ++--
 .github/workflows/sel4test-hw.yml  | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/sel4bench-hw.yml b/.github/workflows/sel4bench-hw.yml
index 0a0aadb9..00cce544 100644
--- a/.github/workflows/sel4bench-hw.yml
+++ b/.github/workflows/sel4bench-hw.yml
@@ -45,7 +45,7 @@ jobs:
     # To reduce the load on GitHub runner numbers and machine queue we cancel
     # any older runs of this workflow for the current PR.
     concurrency:
-      group: ${{ github.workflow }}-sel4bench-pr-build-${{ github.event.number }}
+      group: ${{ github.workflow }}-sel4bench-build-pr-${{ github.event.number }}-${{ strategy.job-index }}
       cancel-in-progress: true
     strategy:
       fail-fast: false
@@ -69,7 +69,7 @@ jobs:
     runs-on: ubuntu-latest
     needs: [build]
     concurrency:
-      group: ${{ github.workflow }}-sel4bench-pr-hw-run-${{ github.event.number }}
+      group: ${{ github.workflow }}-sel4bench-hw-run-pr-${{ github.event.number }}-${{ strategy.job-index }}
       cancel-in-progress: true
     strategy:
       fail-fast: false
diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml
index c40f713c..7a0e20d1 100644
--- a/.github/workflows/sel4test-hw.yml
+++ b/.github/workflows/sel4test-hw.yml
@@ -50,7 +50,7 @@ jobs:
     # To reduce the load (especially on the machine queue) we cancel any older
     # runs of this workflow for the current PR.
     concurrency:
-      group: ${{ github.workflow }}-sel4test-pr-build-${{ github.event.number }}
+      group: ${{ github.workflow }}-sel4test-build-pr-${{ github.event.number }}-${{ strategy.job-index }}
       cancel-in-progress: true
     strategy:
       fail-fast: false
@@ -99,7 +99,7 @@ jobs:
                github.event.action == 'labeled' &&
                github.event.label.name == 'hw-test') }}
     concurrency:
-      group: ${{ github.workflow }}-sel4test-pr-hw-run-${{ github.event.number }}
+      group: ${{ github.workflow }}-sel4test-hw-run-pr-${{ github.event.number }}-${{ strategy.job-index }}
       cancel-in-progress: true
     strategy:
       fail-fast: false

From eabd731897df74eff6150fa2608133b1a1723558 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Thu, 15 Feb 2024 09:48:06 +1100
Subject: [PATCH 10/11] workflows: seltest-sim concurrency at job level

It looks like ${{ github.event.number }} might not exist yet at the
workflow level when the workflow is called, so we move it to the job
level where we know that this info exists.

See also <https://github.com/orgs/community/discussions/107552>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/sel4test-sim.yml | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/sel4test-sim.yml b/.github/workflows/sel4test-sim.yml
index 330f45a5..4254f17e 100644
--- a/.github/workflows/sel4test-sim.yml
+++ b/.github/workflows/sel4test-sim.yml
@@ -11,13 +11,6 @@ name: seL4Test-Sim
 on:
   workflow_call:
 
-# To reduce the load we cancel any older runs of this workflow for the current
-# PR. Ok on the workflow level here, because this workflow does not re-trigger
-# on "labeled" events.
-concurrency:
-  group: ${{ github.workflow }}-sel4sim-pr-${{ github.event.number }}
-  cancel-in-progress: true
-
 jobs:
   sim:
     name: Simulation
@@ -26,6 +19,9 @@ jobs:
       matrix:
         march: [armv7a, armv8a, nehalem, rv32imac, rv64imac]
         compiler: [gcc, clang]
+    concurrency:
+      group: ${{ github.workflow }}-sel4sim-pr-${{ github.event.number }}-${{ strategy.job-index }}
+      cancel-in-progress: true
     steps:
     - uses: seL4/ci-actions/sel4test-sim@master
       with:

From adb6b20208882bad01f3e8b4aa8cb533c6cd819e Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Sat, 17 Feb 2024 12:37:56 +1100
Subject: [PATCH 11/11] workflows: disambiguate artifact names

Since multiple workflows can now be called from the same caller
workflow, these will all end up in the same UI, so we should make
sure the artifact names are not ambiguous.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/sel4bench-hw.yml | 4 ++--
 .github/workflows/sel4test-hw.yml  | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/sel4bench-hw.yml b/.github/workflows/sel4bench-hw.yml
index 00cce544..cf3fc927 100644
--- a/.github/workflows/sel4bench-hw.yml
+++ b/.github/workflows/sel4bench-hw.yml
@@ -60,7 +60,7 @@ jobs:
     - name: Upload images
       uses: actions/upload-artifact@v4
       with:
-        name: images-${{ matrix.march }}
+        name: images-sel4bench-${{ matrix.march }}
         path: '*-images.tar.gz'
 
   hw-run:
@@ -102,7 +102,7 @@ jobs:
       - name: Download image
         uses: actions/download-artifact@v4
         with:
-          name: images-${{ steps.plat.outputs.march }}
+          name: images-sel4bench-${{ steps.plat.outputs.march }}
       - name: Run
         uses: seL4/ci-actions/sel4bench-hw@master
         with:
diff --git a/.github/workflows/sel4test-hw.yml b/.github/workflows/sel4test-hw.yml
index 7a0e20d1..41cfde19 100644
--- a/.github/workflows/sel4test-hw.yml
+++ b/.github/workflows/sel4test-hw.yml
@@ -68,12 +68,12 @@ jobs:
     - name: Upload images
       uses: actions/upload-artifact@v4
       with:
-        name: images-${{ matrix.march }}-${{ matrix.compiler }}
+        name: images-sel4test-${{ matrix.march }}-${{ matrix.compiler }}
         path: '*-images.tar.gz'
     - name: Upload kernel.elf files
       uses: actions/upload-artifact@v4
       with:
-        name: kernel.elf-${{ matrix.march }}-${{ matrix.compiler }}
+        name: kernel.elf-sel4test-${{ matrix.march }}-${{ matrix.compiler }}
         path: '*-kernel.elf'
 
   the_matrix:
@@ -113,7 +113,7 @@ jobs:
       - name: Download image
         uses: actions/download-artifact@v4
         with:
-          name: images-${{ matrix.march }}-${{ matrix.compiler }}
+          name: images-sel4test-${{ matrix.march }}-${{ matrix.compiler }}
       - name: Run
         uses: seL4/ci-actions/sel4test-hw-run@master
         with: