From 55e5bdf7c27ac842aff1758822211b4846fe3c4b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 14 Jun 2024 08:11:15 +0000 Subject: [PATCH] Use all 4 vCPUs on GitHub-hosted runners 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. --- .github/workflows/build-and-test-Linux.yaml | 2 +- .github/workflows/build-and-test-Xen.yaml | 4 +- .github/workflows/codeql-analysis.yml | 8 +- .github/workflows/csmith.yaml | 2 +- .github/workflows/performance.yaml | 4 +- .../pull-request-check-rust-api.yaml | 4 +- .github/workflows/pull-request-checks.yaml | 82 +++++++++---------- .github/workflows/release-packages.yaml | 8 +- 8 files changed, 57 insertions(+), 57 deletions(-) diff --git a/.github/workflows/build-and-test-Linux.yaml b/.github/workflows/build-and-test-Linux.yaml index 30779b0e835..108b225acf3 100644 --- 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 index f7d24efadd0..31ccb2598c6 100644 --- 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 index e8c6a919338..fdbcab27adc 100644 --- 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 index 40e8b9f7b91..564464938bb 100644 --- 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 index 9c56891588d..f054fd6bf73 100644 --- 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 index bb486a13933..ea99785ec25 100644 --- 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 index c6a82b5a1fb..8e1897494a9 100644 --- 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 index c8382afedf3..485112aa43a 100644 --- 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: |