how can i satisfy parallel bounds checker in this example?
it fails with
test.nim(18, 19) Error: cannot prove: y * w8 + x <= len(s) + -1 (bounds check)
strutils
import math
import threadpool
{.experimental: "parallel".}
proc getc() : char = 'b'
let
w = 16
h = 16
w8 = ceil(w / 8).int
var s = 'a'.repeat(w8 * h)
for y in 0..<h:
parallel:
for x in 0..<w8:
s[y*w8+x] = spawn getc()
the example is distilled out of a renderer, where getc is expensive.
test.nim(14, 12) Error: cannot prove: y * w + x <= len(s) + -1 (bounds check)
import strutils
import threadpool
{.experimental: "parallel".}
let
w = 3
h = 3
var s = 'a'.repeat(w*h)
for y in 0..<h:
parallel:
for x in 0..<min(w, s.len - (y*w+w)):
s[y*w+x] = spawn chr(1)
test.nim(8, 7) Error: cannot prove: i <= len(s) + -1 (bounds check)
import threadpool
{.experimental: "parallel".}
var s = "abc"
for i in 0..s.high:
parallel:
s[i] = spawn chr(i)
test.nim(8, 7) Error: (i)..(i) not disjoint from (i)..(i)
import threadpool
{.experimental: "parallel".}
var s = newSeq[char](3)
parallel:
for i in 0..s.high:
s[i] = spawn chr(i)
I must be completely missing the point... :(
In my experience, I never managed to use the parallel construct.
One of the goals of 2020 is to introduce Z3 theorem prover in the compiler and its first use-case would be to prove array accesses (it's not in the milestones yet so hopefuly @Araq can confirm: https://github.com/nim-lang/RFCs/milestone/1).
For multithreading the standard library module is plagued with issues and the plan is to replace it with https://github.com/yglukhov/threadpools.
For high-performance use-case i.e. you also need a smart scheduler and not just a thin wrapper around threads, I suggest you use https://github.com/mratsim/weave (disclaimer: it's my own library).
Note that none of those work with the parallel statement This can be applied to this parallel or also for simple for-loop to avoid checking array accesses at each access but only once before loop-entry.
Fwiw this works fine :P
import threadpool
{.experimental: "parallel".}
proc main =
var s = newSeq[char](3)
parallel:
for i in 0..s.high:
s[i] = spawn chr(i)
echo s
main()
damn you globals! I feel like I should have smelled that...
thanks!
for completeness sake, a working version of the first example (helping the proof engine a bit)
still gonna give weave a try I guess
import strutils
import threadpool
{.experimental: "parallel".}
proc main =
let
w = 16
h = 8
var s = "a".repeat(w*h)
parallel:
## not yet
#for y in 0..<h:
# for x in 0..<w:
# s[y*w+x] = spawn chr(y*w+x)
for i in 0..s.high:
let
x = i mod w
y = i div w
s[i] = spawn chr(y*w+x)
echo s
main()