Use all 4 vCPUs on GitHub-hosted runners

tautschnig · tautschnig · commit 55e5bdf7c27a · 2024-06-17T10:01:43.000Z
Since January GitHub-hosted runners feature a higher vCPU count for Linux and Windows, and also for macos-13. See https://github.blog/2024-01-17-github-hosted-runners-double-the-power-for-open-source/ for the announcement.
diff --git a/.github/workflows/build-and-test-Linux.yaml b/.github/workflows/build-and-test-Linux.yaml
@@ -42,7 +42,7 @@ jobs:
       - name: Build CBMC tools
         run: |
           make -C src minisat2-download
-          make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-diff.dir -j2
+          make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-diff.dir -j4
       - name: Print ccache stats
         run: ccache -s
 
diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml
@@ -41,7 +41,7 @@ jobs:
       - name: Build CBMC tools
         run: |
           make -C src minisat2-download
-          make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-diff.dir -j2
+          make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-diff.dir -j4
       - name: Print ccache stats
         run: ccache -s
 
@@ -58,7 +58,7 @@ jobs:
           ln -s goto-cc src/goto-cc/goto-g++
 
       - name: Compile Xen with CBMC via one-line-scan, and check for goto-cc section
-        run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff  --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen_4_13 xen -j $(nproc)
+        run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff  --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 4 -- make -C xen_4_13 xen -j $(nproc)
         
       - name: Check for goto-cc section in xen-syms binary
         run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc"
diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml
@@ -45,10 +45,10 @@ jobs:
     - name: Build
       run: |
         make -C src minisat2-download
-        make -C src       -j2
-        make -C unit      -j2
-        make -C jbmc/src  -j2
-        make -C jbmc/unit -j2
+        make -C src       -j4
+        make -C unit      -j4
+        make -C jbmc/src  -j4
+        make -C jbmc/unit -j4
 
     - name: Perform CodeQL Analysis
       uses: github/codeql-action/analyze@v3
diff --git a/.github/workflows/csmith.yaml b/.github/workflows/csmith.yaml
@@ -39,7 +39,7 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build with make
         run: |
-          make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-instrument.dir -j2
+          make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-instrument.dir -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run 10 randomly-generated CSmith tests
diff --git a/.github/workflows/performance.yaml b/.github/workflows/performance.yaml
@@ -65,7 +65,7 @@ jobs:
       - name: ccache environment (new variant)
         run: echo "CCACHE_BASEDIR=$PWD/new" >> $GITHUB_ENV
       - name: Build with Ninja (new variant)
-        run: ninja -C new/build -j2
+        run: ninja -C new/build -j4
       - name: Print ccache stats (new variant)
         run: ccache -s
 
@@ -74,7 +74,7 @@ jobs:
       - name: ccache environment (old variant)
         run: echo "CCACHE_BASEDIR=$PWD/old" >> $GITHUB_ENV
       - name: Build with Ninja (old variant)
-        run: ninja -C old/build -j2
+        run: ninja -C old/build -j4
       - name: Print ccache stats (old variant)
         run: ccache -s
 
diff --git a/.github/workflows/pull-request-check-rust-api.yaml b/.github/workflows/pull-request-check-rust-api.yaml
@@ -56,7 +56,7 @@ jobs:
       - name: Configure using CMake
         run: cmake -S. -B${{env.default_build_dir}} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_COMPILER=/usr/bin/clang-13 -DCMAKE_CXX_COMPILER=/usr/bin/clang++-13 -DWITH_JBMC=OFF
       - name: Build with CMake
-        run: cmake --build ${{env.default_build_dir}} -j2 --target cprover-api-cpp
+        run: cmake --build ${{env.default_build_dir}} -j4 --target cprover-api-cpp
       - name: Print ccache stats
         run: ccache -s
       # We won't be running any of the regular regression tests, as these are covered
@@ -97,7 +97,7 @@ jobs:
       - name: Configure using CMake
         run: cmake -S. -B${{env.default_build_dir}} -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ -DWITH_JBMC=OFF
       - name: Build with Ninja
-        run: cd ${{env.default_build_dir}}; ninja -j3 cprover-api-cpp
+        run: cd ${{env.default_build_dir}}; ninja -j4 cprover-api-cpp
       - name: Print ccache stats
         run: ccache -s
       # We won't be running any of the regular regression tests, as these are covered
diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
@@ -50,13 +50,13 @@ jobs:
         run: |
           git clone https://github.com/conp-solutions/riss riss.git
           cmake -Hriss.git -Briss.git/release -DCMAKE_BUILD_TYPE=Release
-          make -C riss.git/release riss-coprocessor-lib-static -j2
-          make -C src -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
-          make -C jbmc/src -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+          make -C riss.git/release riss-coprocessor-lib-static -j4
+          make -C src -j4 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+          make -C jbmc/src -j4 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
 
-          make -C unit -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+          make -C unit -j4 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
 
-          make -C jbmc/unit -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+          make -C jbmc/unit -j4 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
       - name: Print ccache stats
         run: ccache -s
       - name: Checking completeness of help output
@@ -70,10 +70,10 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
       - name: Run regression tests
         run: |
-          make -C regression test-parallel JOBS=2 LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
+          make -C regression test-parallel JOBS=4 LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
           make -C regression/cbmc test-paths-lifo
           env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
-          make -C jbmc/regression test-parallel JOBS=2
+          make -C jbmc/regression test-parallel JOBS=4
       - name: Check cleanup
         run: |
           make -C src clean IPASIR=$PWD/riss.git/riss
@@ -134,10 +134,10 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build with make
         run: |
-          make -C src       -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
-          make -C unit      -j2
-          make -C jbmc/src  -j2
-          make -C jbmc/unit -j2
+          make -C src       -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
+          make -C unit      -j4
+          make -C jbmc/src  -j4
+          make -C jbmc/unit -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run unit tests
@@ -151,10 +151,10 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test
       - name: Run regression tests
         run: |
-          make -C regression test-parallel JOBS=2
+          make -C regression test-parallel JOBS=4
           make -C regression/cbmc test-paths-lifo
           env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
-          make -C jbmc/regression test-parallel JOBS=2
+          make -C jbmc/regression test-parallel JOBS=4
 
   # This job has been copied from the one above it, and modified to only build CBMC
   # and run the `regression/cbmc/` regression tests against Z3. The rest of the tests
@@ -198,7 +198,7 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with make
-        run: make -C src -j2
+        run: make -C src -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run regression/cbmc tests with z3 as the backend
@@ -247,7 +247,7 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja
-        run: ninja -C build -j2
+        run: ninja -C build -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Checking completeness of help output
@@ -258,7 +258,7 @@ jobs:
           ninja package
           ls *.deb
       - name: Run tests
-        run: cd build; ctest . -V -L CORE -j2
+        run: cd build; ctest . -V -L CORE -j4
       - name: Check cleanup
         run: |
           rm -r build
@@ -320,10 +320,10 @@ jobs:
           make -C src/cpp library_check
       - name: Build with make
         run: |
-          make -C src       -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
-          make -C unit      -j2
-          make -C jbmc/src  -j2
-          make -C jbmc/unit -j2
+          make -C src       -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
+          make -C unit      -j4
+          make -C jbmc/src  -j4
+          make -C jbmc/unit -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run unit tests
@@ -337,10 +337,10 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test
       - name: Run regression tests
         run: |
-          make -C regression test-parallel JOBS=2
+          make -C regression test-parallel JOBS=4
           make -C regression/cbmc test-paths-lifo
           env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
-          make -C jbmc/regression test-parallel JOBS=2
+          make -C jbmc/regression test-parallel JOBS=4
 
   # This job takes approximately 22 to 41 minutes
   check-ubuntu-22_04-cmake-gcc:
@@ -385,7 +385,7 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja
-        run: ninja -C build -j2
+        run: ninja -C build -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Check if package building works
@@ -394,7 +394,7 @@ jobs:
           ninja package
           ls *.deb
       - name: Run tests
-        run: cd build; ctest . -V -L CORE -j2
+        run: cd build; ctest . -V -L CORE -j4
 
   # This job takes approximately 26 to 46 minutes
   check-ubuntu-24_04-cmake-gcc-13:
@@ -443,11 +443,11 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja
-        run: ninja -C build -j2
+        run: ninja -C build -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run tests
-        run: cd build; ctest . -V -L CORE -j2
+        run: cd build; ctest . -V -L CORE -j4
 
   # This job takes approximately 30 to 60 minutes
   check-ubuntu-22_04-cmake-gcc-32bit:
@@ -490,11 +490,11 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja
-        run: ninja -C build -j2
+        run: ninja -C build -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run tests
-        run: cd build; ctest . -V -L CORE -j2
+        run: cd build; ctest . -V -L CORE -j4
 
   # This job takes approximately 5 to 24 minutes
   check-ubuntu-20_04-cmake-gcc-KNOWNBUG:
@@ -529,13 +529,13 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja
-        run: ninja -C build -j2
+        run: ninja -C build -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run tests
         run: |
           cd build
-          ctest . -V -L KNOWNBUG -j2
+          ctest . -V -L KNOWNBUG -j4
           export PATH=$PWD/bin:$PATH
           cd ../regression/cbmc
           sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc
@@ -576,11 +576,11 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja
-        run: ninja -C build -j2
+        run: ninja -C build -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run tests
-        run: cd build; ctest . -V -L THOROUGH -j2
+        run: cd build; ctest . -V -L THOROUGH -j4
 
   # This job takes approximately 39 to 69 minutes
   check-macos-13-make-clang:
@@ -732,7 +732,7 @@ jobs:
       - name: Test cbmc
         run: |
           Set-Location build
-          ctest -V -L CORE -C Release . -j2
+          ctest -V -L CORE -C Release . -j4
 
   # This job takes approximately 65 to 84 minutes
   check-vs-2022-make-build-and-test:
@@ -784,15 +784,15 @@ jobs:
       - name: Download minisat with make
         run: make -C src minisat2-download
       - name: Build CBMC with make
-        run: make CXX=clcache BUILD_ENV=MSVC -j2 -C src
+        run: make CXX=clcache BUILD_ENV=MSVC -j4 -C src
       - name: Build unit tests with make
-        run: make CXX=clcache BUILD_ENV=MSVC -j2 -C unit all
+        run: make CXX=clcache BUILD_ENV=MSVC -j4 -C unit all
       - name: Build jbmc with make
         run: |
-          make CXX=clcache -j2 -C jbmc/src setup-submodules
-          make CXX=clcache BUILD_ENV=MSVC -j2 -C jbmc/src
+          make CXX=clcache -j4 -C jbmc/src setup-submodules
+          make CXX=clcache BUILD_ENV=MSVC -j4 -C jbmc/src
       - name: Build JBMC unit tests
-        run: make CXX=clcache BUILD_ENV=MSVC -j2 -C jbmc/unit all
+        run: make CXX=clcache BUILD_ENV=MSVC -j4 -C jbmc/unit all
       - name: Print ccache stats
         run: clcache -s
       - name: Run CBMC and JBMC unit tests
@@ -906,7 +906,7 @@ jobs:
         run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
       - name: Run include-what-you-use
         run: |
-          iwyu_tool -p build/compile_commands.json -j2 | tee includes.txt
+          iwyu_tool -p build/compile_commands.json -j4 | tee includes.txt
           if sed '/minisat2-src/,/^--$/d' includes.txt | grep '^- ' -B1 ; then
             echo "Unnecessary includes found. Use '// IWYU pragma: keep' to override this."
             exit 1
@@ -960,13 +960,13 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=7G
       - name: Execute CMake CBMC build
-        run: cmake --build build -- -j2
+        run: cmake --build build -- -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run CTest and collect coverage statistics
         run: |
           echo "lcov_excl_line = UNREACHABLE" > ~/.lcovrc
-          cmake --build build --target coverage -- -j2
+          cmake --build build --target coverage -- -j4
       - name: Upload coverage statistics to Codecov
         uses: codecov/codecov-action@v4
         with:
diff --git a/.github/workflows/release-packages.yaml b/.github/workflows/release-packages.yaml
@@ -44,11 +44,11 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build using Ninja
-        run: ninja -C build -j2
+        run: ninja -C build -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run CTest
-        run: cd build; ctest . -V -L CORE -C Release -j2
+        run: cd build; ctest . -V -L CORE -C Release -j4
       - name: Create packages
         id: create_packages
         run: |
@@ -118,11 +118,11 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build using Ninja
-        run: ninja -C build -j2
+        run: ninja -C build -j4
       - name: Print ccache stats
         run: ccache -s
       - name: Run CTest
-        run: cd build; ctest . -V -L CORE -C Release -j2
+        run: cd build; ctest . -V -L CORE -C Release -j4
       - name: Create packages
         id: create_packages
         run: |
