arm-hyp+aarch64 spec+proof: make generic in CONFIG_DISABLE_WFI_WFE_TRAPS #977
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Copyright 2021 Proofcraft Pty Ltd | |
| # | |
| # SPDX-License-Identifier: BSD-2-Clause | |
| # On push to master only: run proofs and deploy manifest update. | |
| name: Proofs | |
| on: | |
| push: | |
| branches: | |
| - master | |
| - rt | |
| repository_dispatch: | |
| types: | |
| - manifest-update | |
| # for testing: | |
| workflow_dispatch: | |
| jobs: | |
| code: | |
| name: Freeze Code | |
| if: github.ref == 'refs/heads/master' | |
| runs-on: ubuntu-latest | |
| outputs: | |
| xml: ${{ steps.repo.outputs.xml }} | |
| steps: | |
| - id: repo | |
| uses: seL4/ci-actions/repo-checkout@master | |
| with: | |
| manifest_repo: verification-manifest | |
| manifest: devel.xml | |
| mcs-code: | |
| name: Freeze MCS Code | |
| if: github.ref == 'refs/heads/rt' | |
| runs-on: ubuntu-latest | |
| outputs: | |
| xml: ${{ steps.repo.outputs.xml }} | |
| steps: | |
| - id: repo | |
| uses: seL4/ci-actions/repo-checkout@master | |
| with: | |
| manifest_repo: verification-manifest | |
| manifest: mcs-devel.xml | |
| proofs: | |
| name: Proof | |
| needs: code | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64] | |
| num_domains: ['1', ''] | |
| plat: [''] | |
| include: | |
| - arch: ARM_HYP | |
| plat: exynos5 | |
| - arch: AARCH64 | |
| plat: zynqmp | |
| - arch: AARCH64 | |
| plat: bcm2711 | |
| # test only most recent push: | |
| concurrency: l4v-regression-${{ github.ref }}-${{ strategy.job-index }} | |
| steps: | |
| - name: Proofs | |
| uses: seL4/ci-actions/aws-proofs@master | |
| with: | |
| L4V_ARCH: ${{ matrix.arch }} | |
| L4V_PLAT: ${{ matrix.plat }} | |
| xml: ${{ needs.code.outputs.xml }} | |
| NUM_DOMAINS: ${{ matrix.num_domains }} | |
| env: | |
| AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }} | |
| AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }} | |
| AWS_SSH: ${{ secrets.AWS_SSH }} | |
| - name: Upload kernel builds | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: kernel-builds-${{ matrix.num_domains }}-${{ matrix.arch }}-${{ matrix.plat }} | |
| path: artifacts/kernel-builds | |
| if-no-files-found: ignore | |
| - name: Upload logs | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: logs-${{ matrix.num_domains }}-${{ matrix.arch }}-${{ matrix.plat }} | |
| path: logs.tar.xz | |
| mcs-proofs: | |
| name: MCS Proof | |
| needs: mcs-code | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| arch: [ARM, RISCV64] | |
| num_domains: ['1', ''] | |
| plat: [""] | |
| # test only most recent push: | |
| concurrency: l4v-mcs-regression-${{ github.ref }}-${{ strategy.job-index }} | |
| steps: | |
| - name: Proofs | |
| uses: seL4/ci-actions/aws-proofs@master | |
| with: | |
| L4V_ARCH: ${{ matrix.arch }} | |
| L4V_PLAT: ${{ matrix.plat }} | |
| L4V_FEATURES: MCS | |
| xml: ${{ needs.mcs-code.outputs.xml }} | |
| NUM_DOMAINS: ${{ matrix.num_domains }} | |
| env: | |
| AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }} | |
| AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }} | |
| AWS_SSH: ${{ secrets.AWS_SSH }} | |
| - name: Upload kernel builds | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: mcs-kernel-builds-${{ matrix.num_domains }}-${{ matrix.arch }}-${{ matrix.plat }} | |
| path: artifacts/kernel-builds | |
| if-no-files-found: ignore | |
| - name: Upload logs | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: mcs-logs-${{ matrix.num_domains }}-${{ matrix.arch }}-${{ matrix.plat }} | |
| path: logs.tar.xz | |
| deploy: | |
| name: Deploy manifest | |
| runs-on: ubuntu-latest | |
| needs: [code, proofs] | |
| steps: | |
| - uses: seL4/ci-actions/l4v-deploy@master | |
| with: | |
| xml: ${{ needs.code.outputs.xml }} | |
| env: | |
| GH_SSH: ${{ secrets.CI_SSH }} | |
| - name: Trigger binary verification | |
| uses: seL4/ci-actions/bv-trigger@master | |
| with: | |
| token: ${{ secrets.PRIV_REPO_TOKEN }} | |
| tag: "l4v/proof-deploy/${{ github.event_name }}" | |
| mcs-deploy: | |
| name: Deploy MCS manifest | |
| runs-on: ubuntu-latest | |
| needs: [mcs-code, mcs-proofs] | |
| steps: | |
| - uses: seL4/ci-actions/l4v-deploy@master | |
| with: | |
| xml: ${{ needs.mcs-code.outputs.xml }} | |
| manifest: mcs-devel.xml | |
| env: | |
| GH_SSH: ${{ secrets.CI_SSH }} | |
| # Automatically rebase platform branches on pushes to master. | |
| trigger-rebase: | |
| name: Trigger platform branch rebase | |
| if: github.ref == 'refs/heads/master' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Trigger rebase | |
| uses: peter-evans/repository-dispatch@v3 | |
| with: | |
| event-type: rebase |