-
Notifications
You must be signed in to change notification settings - Fork 6
Expand file tree
/
Copy pathZipBench.lean
More file actions
130 lines (121 loc) · 4.48 KB
/
ZipBench.lean
File metadata and controls
130 lines (121 loc) · 4.48 KB
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
import Zip
/-! Benchmark driver for hyperfine.
Usage:
lake exe bench <operation> <size> <pattern> [level]
Operations:
inflate — native DEFLATE decompression
inflate-ffi — zlib FFI decompression
deflate — native DEFLATE compression (fixed Huffman)
deflate-lazy — native DEFLATE compression (lazy matching)
deflate-ffi — zlib FFI compression
gzip — native gzip decompression
gzip-ffi — zlib FFI gzip decompression
zlib — native zlib decompression
zlib-ffi — zlib FFI zlib decompression
crc32 — native CRC-32
crc32-ffi — zlib FFI CRC-32
adler32 — native Adler-32
adler32-ffi — zlib FFI Adler-32
Patterns: constant, cyclic, prng
Level: 0-9 (default 6, only for compression/inflate)
Examples:
hyperfine 'lake exe bench inflate 1048576 prng 6'
hyperfine '.lake/build/bin/bench inflate 10485760 prng 6' \
'.lake/build/bin/bench inflate-ffi 10485760 prng 6'
hyperfine --parameter-list size 1024,65536,1048576 \
'.lake/build/bin/bench inflate {size} prng 6'
-/
def mkConstantData (size : Nat) : ByteArray := Id.run do
let mut result := ByteArray.empty
for _ in [:size] do
result := result.push 0x42
return result
def mkCyclicData (size : Nat) : ByteArray := Id.run do
let pattern : Array UInt8 := #[0x00, 0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77,
0x88, 0x99, 0xAA, 0xBB, 0xCC, 0xDD, 0xEE, 0xFF]
let mut result := ByteArray.empty
for i in [:size] do
result := result.push pattern[i % 16]!
return result
def mkPrngData (size : Nat) : ByteArray := Id.run do
let mut state : UInt32 := 2463534242
let mut result := ByteArray.empty
for _ in [:size] do
state := state ^^^ (state <<< 13)
state := state ^^^ (state >>> 17)
state := state ^^^ (state <<< 5)
result := result.push (state &&& 0xFF).toUInt8
return result
def generateData (pattern : String) (size : Nat) : IO ByteArray :=
match pattern with
| "constant" => pure (mkConstantData size)
| "cyclic" => pure (mkCyclicData size)
| "prng" => pure (mkPrngData size)
| other => throw (IO.userError s!"unknown pattern: {other}")
def main (args : List String) : IO Unit := do
match args with
| [op, sizeStr, pattern] => run op sizeStr pattern 6
| [op, sizeStr, pattern, levelStr] =>
match levelStr.toNat? with
| some level => run op sizeStr pattern level
| none => usage
| _ => usage
where
usage := throw (IO.userError
"usage: bench <operation> <size> <constant|cyclic|prng> [level]")
run (op sizeStr pattern : String) (level : Nat) : IO Unit := do
let some size := sizeStr.toNat? | usage
let data ← generateData pattern size
match op with
-- Decompression benchmarks (compress with FFI first, then decompress)
| "inflate" =>
let compressed ← RawDeflate.compress data level.toUInt8
match Zip.Native.Inflate.inflate compressed with
| .ok _ => pure ()
| .error e => throw (IO.userError e)
| "inflate-ffi" =>
let compressed ← RawDeflate.compress data level.toUInt8
let _ ← RawDeflate.decompress compressed
pure ()
| "gzip" =>
let compressed ← Gzip.compress data level.toUInt8
match Zip.Native.GzipDecode.decompress compressed with
| .ok _ => pure ()
| .error e => throw (IO.userError e)
| "gzip-ffi" =>
let compressed ← Gzip.compress data level.toUInt8
let _ ← Gzip.decompress compressed
pure ()
| "zlib" =>
let compressed ← Zlib.compress data level.toUInt8
match Zip.Native.ZlibDecode.decompress compressed with
| .ok _ => pure ()
| .error e => throw (IO.userError e)
| "zlib-ffi" =>
let compressed ← Zlib.compress data level.toUInt8
let _ ← Zlib.decompress compressed
pure ()
-- Compression benchmarks
| "deflate" =>
let _ := Zip.Native.Deflate.deflateFixed data
pure ()
| "deflate-lazy" =>
let _ := Zip.Native.Deflate.deflateLazy data
pure ()
| "deflate-ffi" =>
let _ ← RawDeflate.compress data level.toUInt8
pure ()
-- Checksum benchmarks
| "crc32" =>
let _ := Crc32.Native.crc32 0 data
pure ()
| "crc32-ffi" =>
let _ := Checksum.crc32 0 data
pure ()
| "adler32" =>
let _ := Adler32.Native.adler32 1 data
pure ()
| "adler32-ffi" =>
let _ := Checksum.adler32 1 data
pure ()
| other => throw (IO.userError s!"unknown operation: {other}")