Merge branch 'master' into zcu102_virtio_net

.github/workflows/camkes-vm-deploy.yml

@@ -68,7 +68,6 @@ jobs:
         with:
           repository: seL4/machine_queue
           path: machine_queue
-          token: ${{ secrets.PRIV_REPO_TOKEN }}
       - name: Download image
         uses: actions/download-artifact@v3
         with:

.github/workflows/test-hw.yml

@@ -0,0 +1,95 @@
+# Copyright 2021, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+# camkes-vm-examples hardware builds and runs
+#
+# See camkes-vm-hw/builds.yml in the repo seL4/ci-actions for configs.
+
+name: HW
+
+on:
+  # needs PR target for secrets access; guard by requiring label
+  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
+
+jobs:
+  code:
+    name: Freeze Code
+    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') }}
+    outputs:
+      xml: ${{ steps.repo.outputs.xml }}
+    steps:
+    - id: repo
+      uses: seL4/ci-actions/repo-checkout@master
+      with:
+        manifest_repo: camkes-vm-examples-manifest
+        manifest: master.xml
+
+  build:
+    name: Build
+    needs: code
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: true
+      matrix:
+        march: [nehalem, armv7a, armv8a]
+    steps:
+    - uses: seL4/ci-actions/camkes-vm@master
+      with:
+        xml: ${{ needs.code.outputs.xml }}
+        march: ${{ matrix.march }}
+    - name: Upload images
+      uses: actions/upload-artifact@v3
+      with:
+        name: images-${{ matrix.march }}
+        path: '*-images.tar.gz'
+
+  run:
+    name: Hardware
+    runs-on: ubuntu-latest
+    needs: [build]
+    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: true
+      matrix:
+        march: [nehalem, armv7a, armv8a]
+    # do not run concurrently with previous jobs in PRs, but do run concurrently in the build matrix
+    concurrency: camkes-hw-pr-${{ strategy.job-index }}
+    steps:
+      - name: Get machine queue
+        uses: actions/checkout@v4
+        with:
+          repository: seL4/machine_queue
+          path: machine_queue
+      - name: Download image
+        uses: actions/download-artifact@v3
+        with:
+          name: images-${{ matrix.march }}
+      - name: Run
+        uses: seL4/ci-actions/camkes-vm-hw@master
+        with:
+          march: ${{ matrix.march }}
+          index: $${{ strategy.job-index }}
+        env:
+          HW_SSH: ${{ secrets.HW_SSH }}

apps/Arm/vm_introspect/src/cross_vm_connection.c

@@ -19,7 +19,7 @@
 #endif
 
 //example going from linux to native component
-static void sys_ipa_to_pa(void *cookie)
+static void sys_ipa_to_pa(void)
 {
     printf("address from linux is %x\n", *(seL4_Word *)introspect_data);
 

apps/Arm/vm_introspect/src/init_dataport_ram.c

@@ -12,34 +12,37 @@
 #include <sel4vmmplatsupport/guest_memory_util.h>
 #include <vmlinux.h>
 
-extern unsigned long linux_ram_base;
-extern unsigned long linux_ram_size;
-
 extern dataport_caps_handle_t memdev_handle;
 
 static vm_frame_t dataport_memory_iterator(uintptr_t addr, void *cookie)
 {
     cspacepath_t return_frame;
     vm_frame_t frame_result = { seL4_CapNull, seL4_NoRights, 0, 0 };
+    const vm_config_t *vm_config = (const vm_config_t *)cookie;
 
     uintptr_t frame_start = ROUND_DOWN(addr, BIT(seL4_PageBits));
-    if (frame_start < linux_ram_base || frame_start > linux_ram_base + linux_ram_size) {
+    if (frame_start < vm_config->ram.base || frame_start > vm_config->ram.base + vm_config->ram.size) {
         ZF_LOGE("Error: Not dataport ram region");
         return frame_result;
     }
 
-    int page_idx = (frame_start - linux_ram_base) / BIT(seL4_PageBits);
+    int page_idx = (frame_start - vm_config->ram.base) / BIT(seL4_PageBits);
     frame_result.cptr = dataport_get_nth_frame_cap(&memdev_handle, page_idx);
     frame_result.rights = seL4_AllRights;
     frame_result.vaddr = frame_start;
     frame_result.size_bits = seL4_PageBits;
     return frame_result;
 }
 
+/* This overwrites the weak function in the VMM module init_ram */
 void init_ram_module(vm_t *vm, void *cookie)
 {
     int err;
 
-    err = vm_ram_register_at_custom_iterator(vm, linux_ram_base, linux_ram_size, dataport_memory_iterator, NULL);
+    void *reg_cookie = (void *)&vm_config;
+    err = vm_ram_register_at_custom_iterator(vm, vm_config.ram.base,
+                                             vm_config.ram.size,
+                                             dataport_memory_iterator,
+                                             reg_cookie);
     assert(!err);
 }

apps/x86/minimal_64/app_settings.cmake

@@ -10,3 +10,4 @@ cmake_minimum_required(VERSION 3.8.2)
 set(KernelSel4Arch x86_64 CACHE STRING "" FORCE)
 set(KernelX86_64VTX64BitGuests ON CACHE BOOL "" FORCE)
 set(KernelMaxNumNodes 1 CACHE STRING "" FORCE)
+set(LibSel4VMMUseHPET ON CACHE BOOL "" FORCE)