src/Pure/Concurrent/counter.ML
author wenzelm
Sat, 09 Apr 2016 11:35:01 +0200
changeset 62920 a5853334c179
parent 52537 4b5941730bd8
child 68804 cbde6e3b132b
permissions -rw-r--r--
ensure globally unique counter results;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52537
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/counter.ML
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
     3
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
     4
Synchronized counter for unique identifiers > 0.
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
     5
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
     6
NB: ML ticks forwards, JVM ticks backwards.
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
     7
*)
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
     8
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
     9
signature COUNTER =
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    10
sig
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    11
  val make: unit -> unit -> int
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    12
end;
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    13
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    14
structure Counter: COUNTER =
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    15
struct
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    16
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    17
fun make () =
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    18
  let
62920
a5853334c179 ensure globally unique counter results;
wenzelm
parents: 52537
diff changeset
    19
    val counter = Synchronized.var "counter" 0;
52537
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    20
    fun next () =
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    21
      Synchronized.change_result counter
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    22
        (fn i =>
62920
a5853334c179 ensure globally unique counter results;
wenzelm
parents: 52537
diff changeset
    23
          let val j = i + (if Thread_Data.is_virtual then 3 else 2)
52537
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    24
          in (j, j) end);
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    25
  in next end;
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    26
4b5941730bd8 more uniform Counter in ML and Scala;
wenzelm
parents:
diff changeset
    27
end;