package uring

  1. Overview
  2. Docs

Source file heap.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
(*
 * Copyright (c) 2021 Craig Ferguson <me@craigfe.io>
 *
 * Permission to use, copy, modify, and distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

let ( = ) : int -> int -> bool = ( = )
let ( <> ) : int -> int -> bool = ( <> )

type ptr = int
let slot_taken = -1
let free_list_nil = -2

(* [extra_data] is for keeping pointers passed to C alive. *)
type 'a entry =
  | Empty : 'a entry
  | Entry : { data : 'a; extra_data : 'b; mutable ptr : int } -> 'a entry

(* Free-list allocator *)
type 'a t =
  { data: 'a entry array
  (* Pool of potentially-empty data slots. Invariant: an unfreed pointer [p]
     into this array is valid iff [free_tail_relation.(p) = slot_taken]. *)
  ; mutable free_head: ptr
  ; free_tail_relation: ptr array
  (* A linked list of pointers to free slots, with [free_head] being the first
     element and [free_tail_relation] mapping each free slot to the next one.
     Each entry [x] signals a state of the corresponding [data.(x)] slot:

     - [x = slot_taken]: the data slot is taken;
     - [x = free_list_nil]: the data slot is free, and is last to be allocated;
     - [0 <= x < length data]: the data slot is free, and will be allocated before
       [free_tail_relation.(x)].

     The user is given only pointers [p] such that [free_tail_relation.(p) =
     slot_taken]. *)
  ; mutable in_use: int
  }

let ptr = function
  | Entry { ptr = -1; _ } -> invalid_arg "Entry has already been freed!"
  | Entry { ptr; _ } -> ptr
  | Empty -> assert false

let create : type a. int -> a t =
 fun n ->
  if n < 0 || n > Sys.max_array_length then invalid_arg "Heap.create" ;
  (* Every slot is free, and all but the last have a free successor. *)
  let free_head = if n = 0 then free_list_nil else 0 in
  let free_tail_relation = Array.init n succ in
  if n > 0 then free_tail_relation.(n - 1) <- free_list_nil;
  let data =
    (* No slot in [free_tail_relation] is [slot_taken], so initial data is
       inaccessible. *)
    Array.make n Empty
  in
  { data; free_head; free_tail_relation; in_use = 0 }

exception No_space

let alloc t data ~extra_data =
  let ptr = t.free_head in
  if ptr = free_list_nil then raise No_space;
  let entry = Entry { data; extra_data; ptr } in
  t.data.(ptr) <- entry;

  (* Drop [ptr] from the free list. *)
  let tail = t.free_tail_relation.(ptr) in
  t.free_tail_relation.(ptr) <- slot_taken;
  t.free_head <- tail;
  t.in_use <- t.in_use + 1;

  entry

let free t ptr =
  assert (ptr >= 0) (* [alloc] returns only valid pointers. *);
  if ptr >= Array.length t.data then Fmt.invalid_arg "Heap.free: invalid pointer %d" ptr;
  let slot_state = t.free_tail_relation.(ptr) in
  if slot_state <> slot_taken then invalid_arg "Heap.free: pointer already freed";

  (* [t.free_tail_relation.(ptr) = slot_taken], so [t.data.(ptr)] is valid. *)
  let datum =
    match t.data.(ptr) with
    | Empty -> assert false
    | Entry p ->
      p.ptr <- -1;
      p.data
  in

  (* Cons [ptr] to the free-list. *)
  t.free_tail_relation.(ptr) <- t.free_head;
  t.free_head <- ptr;

  (* We've marked this slot as free, so [t.data.(ptr)] is inaccessible. We zero
     it to allow it to be GC-ed. *)
  assert (t.free_tail_relation.(ptr) <> slot_taken);
  t.data.(ptr) <- Empty;         (* Extra-data can be GC'd here *)
  t.in_use <- t.in_use - 1;

  datum

let in_use t = t.in_use
OCaml

Innovation. Community. Security.