You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Joe Moeller (Apr 06 2020 at 16:46):I've programmed in C++ a fair amount. What's aliasing? @sarahzrf
Jules Hedges (Apr 06 2020 at 16:48):That would be references, I guess (and potentially also pointers)
Joe Moeller (Apr 06 2020 at 16:53):There was some discussion on it in another stream since it has to do with Sarah's talk. There she said it had to do with pointers, and I guess something about having two distinct pointers point to the same thing.
Reid Barton (Apr 06 2020 at 16:57):Yeah, basically it refers to when two pointers point to the same thing or overlapping things, particularly when you didn't expect them to.
Joe Moeller (Apr 06 2020 at 16:58):What's the deal with these? What sorts of issues make people say "oh what about aliasing?"
Jules Hedges (Apr 06 2020 at 16:59):(the underlying language-independent concept can also be called names, ie. having multiple names for the same thing)
Jules Hedges (Apr 06 2020 at 17:00):Aliasing + destructive updates = headache. Somebody can do something to , and suddenly has changed. It means you can't reason lexically
Reid Barton (Apr 06 2020 at 17:02):For example if you want to optimize a for loop, you might want to know that updates you make in the body of the for loop don't affect the value of the upper bound of the loop.
James Wood (Apr 06 2020 at 17:08):IIRC, copying an array is a classic thing that can be hit by aliasing. If source and target arrays overlap, the naïve algorithm will at some point start copying the start of the source array again, into the end of the target array (because it starts reading from the start of the target array, which has written over values from the source array).
Reid Barton (Apr 06 2020 at 17:08):Or imagine you are implementing a function that takes pointers to three matrices , , and updates according to the rule .
Reid Barton (Apr 06 2020 at 17:10):The obvious implementation won't work as claimed if the reference is the same as either or (but it's fine if and are the same reference). A variant of James's example.
Joe Moeller (Apr 06 2020 at 17:10):Great, this is all making sense.
Joe Moeller (Apr 06 2020 at 17:10):I had the sense that it should be a thing I encountered but just never saw a name put to it, and that's exactly what it was!
Paolo Capriotti (Apr 06 2020 at 21:06):the standard issue with aliasing is that if the compiler cannot prove that pointers point to different things, it might have to reload a value from memory even when not necessary, because it cannot be sure that it hasn't been written by previous instructions
Paolo Capriotti (Apr 06 2020 at 21:07):so C for example has a keyword (restrict IIRC) to instruct the compiler that it is allowed to assume that two pointers point to non-overlapping areas, so that certain optimisations can be applied
sarahzrf (Apr 06 2020 at 23:06):reid's example ties in great with the kind of thing i would want to illustrate, actually
sarahzrf (Apr 06 2020 at 23:07):the kind of place you use separation logic in practice is generally for writing down specifications of the behavior of programs, such as saying "this program really does add matrices"
sarahzrf (Apr 06 2020 at 23:07):but of course, if you wrote the obvious implementation, that specification just isn't true—what if the matrices you pass in alias?
sarahzrf (Apr 06 2020 at 23:08):except that in separation logic, you can use "separating conjunction" instead of ordinary conjunction when necessary, and when you do so, you implicitly rule out such cases in your premise
sarahzrf (Apr 06 2020 at 23:09):so that the case you naïvely had in mind now really is what you're saying with your specification
sarahzrf (Apr 06 2020 at 23:10):the "separation" is as in "separation of the resources underlying the matrices from one another"