src/Pure/Concurrent/multithreading.scala
author haftmann
Wed, 21 May 2025 20:13:43 +0200
changeset 82648 35e40c60c680
parent 79759 5492439ffe89
permissions -rw-r--r--
typo
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
79603
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Concurrent/multithreading.scala
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
     3
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
     4
Multithreading in Isabelle/Scala.
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
     5
*/
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
     6
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
     7
package isabelle
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
     8
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
     9
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
    10
object Multithreading {
79604
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    11
  /* physical processors */
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    12
79605
83627a092fbf more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents: 79604
diff changeset
    13
  // slightly different from Poly/ML (more accurate)
79604
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    14
  def num_processors(ssh: SSH.System = SSH.Local): Int =
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    15
    if (ssh.isabelle_platform.is_macos) {
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    16
      val result = ssh.execute("sysctl -n hw.physicalcpu").check
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    17
      Library.trim_line(result.out) match {
79613
7a432595fb66 more robust defaults;
wenzelm
parents: 79607
diff changeset
    18
        case Value.Int(n) => n max 1
79604
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    19
        case _ => 1
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    20
      }
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    21
    }
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    22
    else {
79605
83627a092fbf more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents: 79604
diff changeset
    23
      val Physical = """^\s*physical id\s*:\s*(\d+)\s*$""".r
83627a092fbf more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents: 79604
diff changeset
    24
      val Cores = """^\s*cpu cores\s*:\s*(\d+)\s*$""".r
83627a092fbf more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents: 79604
diff changeset
    25
79758
wenzelm
parents: 79650
diff changeset
    26
      val physical_cores: Int = {
wenzelm
parents: 79650
diff changeset
    27
        var physical: Option[Int] = None
wenzelm
parents: 79650
diff changeset
    28
        var cores = Map.empty[Int, Int]
79605
83627a092fbf more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents: 79604
diff changeset
    29
79758
wenzelm
parents: 79650
diff changeset
    30
        val result = ssh.execute("cat /proc/cpuinfo").check
wenzelm
parents: 79650
diff changeset
    31
        for (line <- Library.trim_split_lines(result.out)) {
wenzelm
parents: 79650
diff changeset
    32
          line match {
wenzelm
parents: 79650
diff changeset
    33
            case Physical(Value.Int(i)) => physical = Some(i)
wenzelm
parents: 79650
diff changeset
    34
            case Cores(Value.Int(i))
wenzelm
parents: 79650
diff changeset
    35
              if physical.isDefined && !cores.isDefinedAt(physical.get) =>
wenzelm
parents: 79650
diff changeset
    36
              cores = cores + (physical.get -> i)
wenzelm
parents: 79650
diff changeset
    37
            case _ =>
wenzelm
parents: 79650
diff changeset
    38
          }
79605
83627a092fbf more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents: 79604
diff changeset
    39
        }
79758
wenzelm
parents: 79650
diff changeset
    40
        cores.valuesIterator.sum
79605
83627a092fbf more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents: 79604
diff changeset
    41
      }
79759
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    42
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    43
      def logical_cores(): Int =
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    44
        if (ssh.is_local) Runtime.getRuntime.availableProcessors()
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    45
        else {
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    46
          Library.trim_line(ssh.execute("nproc").check.out) match {
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    47
            case Value.Nat(n) => n
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    48
            case _ => 1
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    49
          }
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    50
        }
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    51
5492439ffe89 more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents: 79758
diff changeset
    52
      if (physical_cores > 0) physical_cores else logical_cores()
79604
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    53
    }
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    54
0e8ac7db1f4d clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents: 79603
diff changeset
    55
79603
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
    56
  /* max_threads */
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
    57
79650
65ef68bab8d6 clarified modules: centralize default policy;
wenzelm
parents: 79613
diff changeset
    58
  def max_threads(
65ef68bab8d6 clarified modules: centralize default policy;
wenzelm
parents: 79613
diff changeset
    59
    value: Int = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0,
65ef68bab8d6 clarified modules: centralize default policy;
wenzelm
parents: 79613
diff changeset
    60
    default: => Int = num_processors()
65ef68bab8d6 clarified modules: centralize default policy;
wenzelm
parents: 79613
diff changeset
    61
  ): Int = {
65ef68bab8d6 clarified modules: centralize default policy;
wenzelm
parents: 79613
diff changeset
    62
    if (value > 0) value else (default max 1) min 8
79603
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
    63
  }
9f002cdb6b8d clarified modules, following Isabelle/ML;
wenzelm
parents:
diff changeset
    64
}