Just to be clear that 20ns is a cache hit by virtue of it being a runtime check
But @Mason apparently has an idea for making it a compile time check via a custom interpreter, so we might soon eliminate that 20ns altogether.
Just to be clear that 20ns is a cache hit by virtue of it being a runtime check
But @Mason apparently has an idea for making it a compile time check via a custom interpreter, so we might soon eliminate that 20ns altogether.
You know statements like these are catnip for me. I couldn’t resist: Perform borrow checking at compile time by MasonProtter · Pull Request #37 · MilesCranmer/BorrowChecker.jl · GitHub
This PR lets all the borrow checking happen at compile time, so there’s no runtime overhead.
Yeah ![]()
Ok BorrowChecker now has the option to recurse into callees, meaning you only need annotate the entrypoint to borrow check an entire dependency tree!
import BorrowChecker as BC
# default: (ONLY borrow checks foo(), not bar())
BC.@auto scope=:function foo() = bar()
# all functions defined in the module:
BC.@auto scope=:module foo() = bar()
# all functions not in Base or Core
BC.@auto scope=:user foo() = bar()
# everything
BC.@auto scope=:all foo() = bar()
This is now live too: the borrow checker completely disappears from the compiled function after validating it:
julia> BorrowChecker.@auto scope=:all f(x) = sin(x)
f (generic function with 1 method)
julia> @btime f(1.0)
1.250 ns (0 allocations: 0 bytes)
0.8414709848078965
Thanks @Mason!
This is impressive! I‘m a little confused by the opening example though. Isn‘t Julia semantics that the function
function f()
x = [1, 2, 3]
y = x
push!(x, 4)
return y
end
is completely equivalent to
function f()
x = [1, 2, 3]
push!(x, 4)
return x
end
So the first being an error is changing what is considered valid code without it being an actual race condition, or am I misunderstanding something? Conversely, if the call to push! were asynchronous, both versions would be problematic but would the second one be flagged as an error?
julia and rust have different phylosophi as of variable name, in julia they are just names, in rust they actually are owners. Having a borrow checker will help about race conditions of course but not the compiler ( besides maybe error handling ) ie making sure your julia code is borrow-friendly doesn’t mean the codegen will be better, however it is useful for devs used to rust phylosophi and as such will cancel valid julia code to respect this.
Yes, that’s right. But this borrow checking package enforces extra rigidity on top of regular julia semantics. In this case, it’s to no benefit, but there are cases where it can catch things.
Do you think it’s possible to implement rust’s Drop trait on top of this, allowing us to clear up a value at the end of its scope rather than waiting for its finaliser to be called at some arbitrary point in the future?
Yes, that’d be quite possible. Currently the package doesn’t do any code transformations or re-interpretation, it just does analysis and early errors, but we could use to analysis to inform some pretty neat transformations.
I think Miles has said before he’s not too interested in doing that himself, as he only cares about this for correctness checking, but he’s open to others contributing it.
Just to clarify, I’m not not interested, it’s just I have a chronic time deficiency and there are too many fires to put out
But if someone’s interested in working this I’d be happy to help!
But yes my original motivation for building this is mainly to help detect unsafe patterns inside SymbolicRegression.jl. I mean better GC would be great of course but other problems have kept me up more nights: so far it’s been type instability (resulting in DispatchDoctor.jl), unexpected performance regressions (resulting in AirspeedVelocity.jl), as well as some data races that took over a year to pinpoint (resulting in this package).
I think @yolhan_mannes and @Mason explain it nicely.
And yeah, you’re reading it correctly. In plain Julia, both versions are equivalent after compilation. The borrow checker is intentionally stricter than Julia semantics. It’s more like a “correctness mode” that forces your code into a shape where whole classes of aliasing bugs and thread races become impossible (modulo {untracked code, bugs in the borrow checker, etc.} of course).
The toy y = x; push!(x, ...) example is showing the core rule: if you create a live alias to a mutable object, you are no longer allowed to mutate using the original binding. You have to copy x or otherwise never refer to x again, since it is effectively now “owned” by y. That can feel conservative in purely single-threaded code, but it lines up with the design you’d want if you later introduce tasks.
Re: your async question: if push! were actually “spawned” (or otherwise could run concurrently), then both versions are problematic in spirit, because you’d have mutation of the same object potentially overlapping with other uses. A checker that tracks “mutable borrow escapes into another task” should flag that, regardless of whether you wrote y = x explicitly. For example, maybe I forgot to copy a mutable when capturing it in a closure:
import BorrowChecker as BC
BC.@auto function foo1()
x = [1, 2, 3]
task = @async begin
for i in 4:8
push!(x, i)
end
return sum(x)
end
y = copy(x) # oops, x is already getting mutated!
sum_x = fetch(task)
return sum_x, y
end
Here, I capture an object [1, 2, 3] within the task. But x is still live, because I then refer to it later. That’s not allowed, because that first push! might happen before I do the copy.
So the correct solution would be to copy before capturing in the @async block:
BC.@auto function foo2()
x = [1, 2, 3]
y = copy(x)
task = @async begin
for i in 4:8
push!(x, i)
end
return sum(x)
end
sum_x = fetch(task)
return sum_x, y
end
Which avoids the data race.
And if you run this in the REPL, you should normally see that BorrowChecker.jl would correctly flag the first:
julia> foo1()
ERROR: BorrowCheckError for specialization Tuple{typeof(foo1)}
But, annoyingly, this also flags foo2 because Julia tasks involve storing the task object in a globally accessible mutable queue, which of course violates borrowing rules due to the escape
UGH. So we might need to special-case things even though its technically an unsafe pattern.
As with rust lots of useful things need to be hidden behind an unsafe like construct
Check this out. BorrowChecker.jl plugged into JETLS.jl, so you can get borrow checker hints just like in Rust:
woah, how did you do that? I’m interested in incorporating ExplicitImports with JETLS
It’s basically this sketchy and hardcoded monkey patch of JET.jl and JETLS.jl to include BorrowChecker.jl errors. Not very modular sadly! We will need a better way.
But @aviatesk said he’s open to a plugin system that would let us add these! See slack thread. Then in principle you could just add different hooks to your VSCode settings I guess.
Edit: plugin system PR: Create a plugin system by MilesCranmer · Pull Request #494 · aviatesk/JETLS.jl · GitHub
Quick note that @auto has been soft deprecated in favor of @safe.
Also, there’s now an @unsafe macro now to disable the borrow checker for a specific part of code. I found this necessary for actual usage in library code. @unsafe works in a similar way to Rust’s:
julia> using BorrowChecker
julia> @safe function add_halves!(a::Vector)
n = length(a) ÷ 2
@unsafe begin # (= I checked this manually and am sure it's safe)
left = @view a[1:n]
right = @view a[n+1:2n]
left .+= right
end
return a
end
add_halves! (generic function with 1 method)
julia> add_halves!([1, 2, 3, 4, 5, 6])
6-element Vector{Int64}:
5
7
9
4
5
6