Add a meeting Rate this page

A

So, let's see so there is this. Also this assertion failure we could either. I can either walk you through the idea or we can try to debug this together or both um I'm not for either all right. Why don't? We go through the first high level idea and then um proceed to. Maybe debugging will give us a nice like way to explore the code in a purposeful fashion, but um the uh right so the idea so.

A

Actually, what I um trying to decide, I guess I'll, walk through the what's on the branch exactly and then we'll go from there. I have a little I, like my. I have a different branch where I refactored the code to isolate out the stack logic and I think it's easier to follow, but it might be confusing um if I started with that, so I won't.

A

uh What do I want? I want select mod, so I don't. This is annoying dude. Do you have this problem? Maybe there's I should figure out how there's got to be a way to tell it like I'm not.

B

Interested.

A

In all of them, please put them at the bottom of the list. Yeah.

B

I have that problem, sometimes um yeah, I don't know it turns.

A

Out like every unique substring appears in lvm somewhere uh and often many.

B

Times yeah, it doesn't surprise me.

A

Also, we do use a lot of the same words like also both.

B

Compilers.

A

Anyway, okay, so right, so trade evaluation is a fairly straightforward process in which we do a basically a sort of depth. First search down to try to decide if a trait might be implemented, it's not entirely clear why it exists in addition to the other mode of evaluating traits, except that nico didn't know what what he was doing when he first implemented this code and it grew into this structure. uh But that's all right. um It has.

B

Wait so what do you mean by different than the other way of evaluating so.

A

There's two ways that the compiler evaluates traits they're connected and interrelated, and not entirely separable. There's the fulfillment context and the evaluation logic, okay and the fulfillment context, sort of does a I'll call it a breath. First search.

A

That's that's not really true, that's actually maybe just kind of misleading, but it basically keeps a queue of work to do and if you have to prove that one impul is or that t implements some trait some type t implements some trait it will figure out which impul you're using and take the where clauses from that impul and add them to that queue right. So that's like one distinct step. That's trait selection, or I call that trade selection right.

C

uh

A

Is picking which input you're going to use, but it does that without necessarily knowing that the where clauses are satisfied, the problem is- and this is where the two systems arose. That was the first inspiration for how it should work and in old rust when that was implemented like we didn't have, we didn't even have and actually didn't, really have where clauses for the most part. So it wasn't that complicated to do uh and we had where clauses, I guess, but we did, we didn't, have uh our coherence.

A

Rules were much simpler, such that, like basically, only one at most one input would unify, so that was fairly straightforward and then, when we tried to extend it to allow for things like, I have an impul for all things that are cloned and an impulse for something. That's not cloned.

A

uh We had this problem that we couldn't pick in the same way, and so we added trait evaluation, which basically tries to figure out, is this type it does. Instead of instead of like unrolling and pushing things onto the queue it tries to go down all the way and figure out. Do all the where clauses are they all satisfied all the way down? Can I just fully prove this out um and it's not always it's sort of a try value right like it comes back with?

A

Well, it comes back with an evaluation result which is um either like yes or probably, but there's some region relationships. I couldn't verify because I don't know how to do that uh or I couldn't tell one way or the other or some other variation of I couldn't tell one way or the other or uh you know. No, it does not. There's no such impulse that could potentially apply and recur is like another thing, um and so that's for cycles and stuff, um and so right. So the code is fairly straightforward, like proving the trait predicate.

A

So we have this stack. I guess that's the other thing. uh We keep a stack of the context in which we had to prove something um when we're doing the at the fulfillment context level. That stack is always empty. Like everything the fulfillment context starts to work on is the top of the root of the stack it's. The first thing is finding the impul.

A

That applies for a given thing, but when we're doing the evaluation, we can go deeper in where we're processing the where clause and then the where clauses of the where clause and so forth- um and this is the stack type um it is well. Actually, this is an iterator. This is the stack type um and it's just a linked list, so it has a reference to the previous element on the stack and then this is the top of the stack.

A

um It's a link.

B

Increase your font size like one two.

A

Yeah good point.

B

um Maybe uh control plus, I think.

A

Let's zoom in does that work.

A

Okay, yeah! Is that better? Yes, thank you uh so yeah. This is the top of the stack. We push things on by calling well by building another one of these structs with a reference to the previous top of the stack, so it actually walks up the real program stack as well, um and.

A

um

B

Jumping.

A

Like my.

B

Chalk hat on I'm like thinking about how this is similar and different.

A

Yeah, it's similar to the recursive silver. You know, but different in certain respects that I'm about to go into um so, and but this pr is, among other things, moving them moving the evaluation model closer and closer to how the recursive solver works and like to shift gears to chalk ever so slightly.

A

I haven't fully mapped this out in my head yet, but I do think one way to get chalk into rusty, as we were sort of discussing, is to tweak how rusty works so that it uses the evaluation more and more, which we've also been moving from time to time for various.

C

Other reasons.

A

And then, but like the more we're able to lean on this, instead of the fulfillment model, the closer we're getting to how chalk's going to interact and that could be useful and then we can also bring like lessons from chalk to make this evaluation system better because it has certain limitations.

A

um So right evaluation starts here at this evaluate trade, predicate recursively, um which gets called by some other. It doesn't really start here, but the interesting stuff starts here uh and first thing it does is push so here's the old stack, we're gonna push push onto the stack, which means make a new struct. If you go through you'll, see it just instantiates one of those instances. um We track the depth and this will be important. We track this depth. First number, that's familiar to you from chalk, I'm sure it's just a counter that increments.

A

The difference between them is when things get popped off the stack the depth goes down, but the depth first number never changes, or it just keeps going it's monotonic, um which is useful. uh So then we do some I'm going to ignore this. Caching, although it's going to turn out to be pretty important, but for now, let's ignore it, because the whole the whole bug is around caching, so it will be important, but um we look for a cycle that doesn't well.

A

That will also become relevant, but let's ignore it for the moment, uh and then we do this thing evaluate stack so this what does the actual work? This is like. Okay, I have a stack. I want to check if the thing on the top of the stack is true, false, whatever true false are unknown, and um I've already had the cat. I've already looked for cycles and checked the cache and done all that stuff just do the actual work. um So what does it do um ignore this stuff?

A

This has to do with coherence, uh and it's basically it's. It's basically uh makes us fail to.

A

I don't know I forget what this does. Who cares something with coherence and like making us not try to prove things? That would be bad for coherence. um This is the interesting part. So here we call candidate from obligation.

A

What that does, is it finds so a candidate in the parlance of this code is basically a way to prove that a trait holds, and so.

C

This is.

A

The this is the point where this is one of the points where we break from chalk and from a traditional like a more capable deer improver, uh because really what we should probably get back here is a vector of candidates. um There can be many ways to prove that the thing that the tree holds and it.

C

Sort of doesn't matter.

A

Which one we do as long as we have one. However, we force ourselves to return one with some horrible heuristics that you're vaguely familiar with and that we will not go into here because they're not relevant, um and so we get back. We get back one of these options. Either we get back a selection candidate.

A

That means we found what we think of as the right way to go. We found the impul. Let's take the easy case, there's exactly one impul that unifies and might apply this will this will information about that input will be in c. If we get back none, it means there were ways to go, but we couldn't figure out which one there were too many impulse that might have applied and we couldn't narrow it down.

A

That could happen if there's inference variables, for example like if we, if we're trying to prove that question mark t, implements a trait that could be any impul, so so long as there's at least two impulse we're stuck um uh or where clauses stuff like that overflow is overflow, and otherwise, if we get back air here, it means there was no impul. That might apply, there was no candidate. We couldn't find one.

B

Is it just me or would like an enum here, make more sense than a nested option result.

A

It's not just you um yeah, I don't know, we might use question mark yeah this yeah. There are some things that could be improved uh for one thing I noticed as we're walking through here that also like air is used somewhat differently right. Like for evaluation, you can have an okay with a evaluated to error and an error is just used for overflow, but for candidate error means no candidates, which is a little confusing uh yeah you're, not wrong. So nonetheless, the happy path is. We found a candidate we jump in to evaluate candidate.

A

What does evaluate candidate? Do um evaluation probe just prevents muta uh inference, variable side effects from leaking outside, so what confirm candidate does? Is it takes the like? We figured out which impul applies confirm candidate will unify all the types from the impul with the types of the thing we're trying to prove.

A

So as an example, if we had an impul, if we were trying to prove like option of question, mark t is foo and there's exactly one impul of foo. That was like impul fu for option of i32.

A

Then this confirmed candidate would unify question mark t with i32.

A

More commonly it goes the other way that we have a type that we know and an inference variable which arises out of the input like we replace t with a fresh infant's variable as part of the conformation, and then we unify them and so t becomes unified with I-32 i32.

A

But then we get back from this a list of um well, we get back, what's called an impulse source which is kind of related to the canon. It's sort of the information. But the main thing that's in there that we're interested in is this nested obligations, which is basically the where clauses, and so then we're going to go, recursively, evaluate them and say: like okay, well, the impul applied we were able to unify the impul. Everything succeeded now, let's check if the where clauses apply and that's that's the whole recursive concept.

A

So far, so good.

B

um

A

All right we're going to pop back up. This is actually the root of evaluation, evaluate predicate.

A

um Not I sure before I showed you like, evaluate trade predicate which is called here, but that's just one case, because there's different kinds of predicates but most of the others are not that interesting like if, for example, we're forced to prove some region relationship, we can just say yeah. That seems good.

A

It's good as far as we know, uh and uh there's like some other stuff here, but it sort of bottoms out to this is the main case. Okay, um so jumping back. I want to talk about the caching and the cycles.

A

Let's talk about cycles first, um so what do we do? Where did I that's? The other problem I have with vs code is.

A

The back is like it's good, because it has like every place my cursor landed, but sometimes it takes me a while to find the one. I I want. Okay.

B

Now, there's a pack option so.

A

Oh yeah, I don't know how you live without that control.

C

Dash.

A

On mac, but it changes on other platforms, um so check evaluation, cache, uh that's not what we're talking about talking about check, evaluation cycle, um so we have the stack and the main reason we actually have. The stack is so that we can sorry just having a little thought. Oh right, I remember now so that we can detect cycles um and what do we do?

A

We iterate it's very simple: we basically iterate up the stack looking for something where we have the same thing we have to prove or the environment is the same, and the thing we're trying to prove is the same: fresh trait ref, uh that's an old version of canonicalization where inference variables get replaced with a like an integer that is ordered by their appearance.

A

It's basically the same as canonicalization. We just have two ways to do it that are similar but different, uh because this one was done. First, um that's great! Yes, isn't it uh so um right? So we we iterate over the stack we look and see if any of them are there. If there is one we extract its depth and we say: okay, we found a cycle, and this is where the assertion is failing. As an aside or one of the places it might be failing, and then we call update reach depth. So what is that?

A

What happens is for everything on the stack we are tracking. What is the.

B

Oh.

A

What is the f up and down are always kind of problematic. What's the oldest thing on the stack that you depended on right? So if I, if, if there's no cycle, then it's just going to be yourself basically, so I depend on in order to prove that t implemented foo, I had to prove that to implement flu. That seems fine, but if you end up with a cycle like usually with auto traits, here's an example right here like you're proving foo of t is send.

A

That requires proving bar of t is n and maybe bar has a foo inside of it. So then I have to prove the foo of t is send again.

A

Then I would update the reached depth of bar of t to be equal to the depth of the foo of t.

A

So if this was zero- and that was one- and that's well- that's two, but it does never get pushed then this would have a reach depth of zero um and that's useful, because that tells me that, in order that tells me that, um especially for the co-inductive cases, bar of send is true so long as the things that were higher on the stack up to the reached depth are also true, it's kind of conditionally, true um or provisionally. True right. So that's what the checking cycle basically! Does it tracks? How high did you go?

A

It checks if it's a co-inductive, if everything in that cycle is co-inductive, in which case it's okay, but we updated the depth. Otherwise it does this evaluated to recur, which um either way we're going to stop right. So either we reach the cycle, which will be treated as a kind of error or we are considering it okay, but we we had to mark things on the stack to indicate that was like a provisional okay, um and so that's where we come to this caching business.

A

So then, assuming zooming out now, if we were doing that this case of fubar foo when we're processing foo the first time, there's no cycle, we go into the evaluate stack. We come in here for bar no cycle. We go into evaluate stack. Now we come back for foo. We hit a cycle, we're going to mark bars, having reached an earlier depth and return, and then we're going to come back and now we're still at the point where we're proving bar.

A

So we basically will have proved evaluate stack, will have returned okay, because that cycle was checked and returned okay, so we now think okay bar is proven and ignore this for a second we're going to look here at what depth did you reach, and the question is if it is, uh if, if you never depended on anything above you in the stack or older than you, I should really stick to older anything older than you on the stack.

A

Then you're kind of self-complete right. So so you're done. But in our case, where we're processing bar bar depended on foo, which was older in the stack and therefore um we can't consider that to be completely evaluated. So we use this thing called a provisional cache and the idea is that, essentially attached to the stack itself, we have a cache. We have several caches at different layers depending on how how true that thing is, but for our purpose for this particular bug, we can just think about two caches. There's like the global cache for stuff.

A

That we really know is true and then there's the provisional cache which is attached to our stack, which is saying we proved this to be true, but it was subject to something. That's still on the stack.

A

um So it's true it's true. Unless that thing turns out to be false um and we'll track, we pass in what was our depth first number.

C

What.

A

Was the depth that we're dependent on and what was the result, um and now, when you come back, if, for example, you had foo of t had to prove bar of t, then bar of t would be added as a provisional cash hit because of the cycle, but now suppose that then foo has to prove baz and baz has to prove bar as well.

A

Okay, uh now we have another cycle because or if we went and recursively processed bar again, if we ignore the caching we would we would get a cycle just like before, where bar would depend on foo and it would mark um bar would depend on foo. Let me put the comments, because I'm it's clear in my there's a visualization in my brain, but it may not be in yours.

A

uh I'm gonna write out, though,.

B

I think I can do it, but for the people who are watching the recording, it would definitely be helpful. That's.

A

What I'm imagining um so we basically had. Let's, let's replay it, we started out with foo we pushed bar into the stack we pushed foo. We got a cycle right, then we marked bar as reached depth, equals zero um processing that cycle, and we marked this as okay, then here we would consider this okay, because all of its children are okay, but then suppose that for foo, let's add like depends on bar bass.

A

So in order to prove foo was true, we had to prove bar and best, so we started by proving bar which we have done, and then we went to prove baz.

A

um Baz, let's say depends on bar okay, so then, what we're gonna do I'm just going to ignore? Caching, for a second pretend we did everything with no caches at all, then we would go to bar and we would say: okay well bar depends on foo just like before we'll push foo, here's a cycle.

A

You could think of this. As a cycle reached depth equals zero. Okay, you can sort of see I'm evolving a weird notation here. uh This would be the same. We we again, we found a cycle. The depth of the thing was zero, so we reached up zero. We consider ourselves. Okay, this guy is going to say, okay.

A

Well, my reach depth is zero because I have a child that reached so the way this works in chalk and the way I would like to think of it is that your result is not just okay or error, but your result comes with the depth that you reached or something like that. That's not the way we've implemented it here, because it was stapled on to an older system that didn't understand this stuff.

A

So the the depth is like stored in the stack as a kind of side, mutation thing uh and and the only the okay is passed back. We should probably refactor that at some point, but what that means is the way this is actually working.

A

Is that at each point we are initializing the reach depth, so it starts out with the depth of the current node right um and then, when we find the cycle before, we've actually returned we're going to go back here and update these to be equal to the the minimum of their previous value and the cycle we just encountered.

A

Okay and then we're going to return, and then here we're going to return- and here, let's say, there's no more dependencies, so we return, and- and now we get up to here- and we can return our reach depth here- started out as zero and it never changed because nobody was able to reach past the top of the stack or the bottom of the stick. Rather um the root of the stack and that's fine, that's how this would work with no caching.

A

uh So what do we do now? What do we do instead? um Or what do we do? The problem? Is we repeated some some effort here and that's one problem. Another problem is we would like to cache all these results so that if anybody uh and another function should try to prove the same thing, they don't have to do the work again either.

A

um We would like to do both those things, so we like to save ourselves some work while we're doing it and save future callers some work too, and those are a little bit different. So the way that we do this is we'll. First, just talk about saving our self-work.

A

um When we see a cycle, or rather let's first talk about saving other people work, I guess so there's a global cache of things that we've proven true right and norm like when we get an okay result. We like to put things in that cache as soon as we can, because then everybody else can make use of them.

A

um The problem is, we can't put these internal nodes like we can't put this foo in there, for example, we did find it it's okay, but that was part of this big cycle thing and it's only okay, if all the other parts of the cycle turn out to be okay, the same with bar as it happens, because because it's reached depth was older than itself, it's a provisionally.

A

Okay result: it can't be cached globally yet because maybe it will turn out that baz is not true and we don't know that yet um and the same with baz.

A

Well, if with as it turns out it's the last thing, we have to prove so it would be okay, but we didn't figure that out yet either um so so what we do is we have this provisional cache and if we kind of replay when we got to the point where we proved bar to be true not for cycles, we don't do it there, all the you could, I guess anyway, it doesn't matter instead of searching the stack.

A

If you wanted, you could seed the provisional cache now that I think about it, probably be more efficient, um but in any case, uh what we do instead is we when we see bar- and we see that it's okay, but we see that the depth is older than ourselves. That's this path!

A

uh We insert into the provisional cache this entry, so we'll say: okay bar is okay with a reached depth of zero and let me just walk into the provisional cache for a second. What does that? Look like cache is very simple: it's a um well that's interesting! Well, anyway, uh here's a bit of break from chalk. Also, the key is the thing we're trying to prove. We don't store the environment because we assume the entire stack has a single environment. That's stupid.

A

We should fix that um small thing uh and the value is this provisional evaluation? So what was the result? What was the depth first number, from which I tried to prove it that's useful later, and what depth did it wind up depending on what was the oldest thing? It depended on okay, so we're going to insert that in the cache and now when baz comes and wants to prove bar, it's going to find it in the cache here.

A

Get provisional get provisional is going to oops here. Just do a just a hash map look up. It returns a provisional evaluation and the main thing is. We can return the result, but we have to act as if we reached the depth of that cache value because effectively we're replaying this search, we're just short-circuiting it to the to the result. So if we redo this, what would happen with the cache just to like play it through and not require you to hold state in your mind?

A

um We would start here. We would say this is okay. We would cache provisionally.

A

We would go to prove bar baz, we would say okay, this has a reach depth of 1. To start, we know that it depends on bar, we would come to bar, we would say cash hit, it's ok or it has a reach depth of zero. That would cause us to go back up and tweak this to zero. We would then return. Okay, this would return okay and then this would get cached too, because um it is also a okay result that depends on something older in this deck.

A

Okay and then we would get up to foo and at that point foo now has its okay result, but, unlike these other.

A

Sub results: the reach depth of foo is not older than itself, so we've actually found the start of the cycle. um It happens to be the root node, but we don't that's, not important, um and so that means that not only is foo okay, but we know that these provisional cache results are also true, um and so now that's this case.

A

Okay, the reached depth is no older than our depth. um That's what that's saying uh it's greater than or equal to so it's younger than uh or equal to um it.

B

Actually will not.

A

Like.

B

That's backwards tower, I think, but no that's right.

A

Yeah, that's right, um it's I think it. I think. If I were to write this again, I would write if stack, that up is less than or equal to, but yeah I find greater than or equal to be. A very my mind wants small things on the left, uh but anyway that's how it was written. I don't know so by me, I'm sure, but uh it made sense at the time, so the um what does it do right, insert evaluation cache!

A

That's the global cache, unlike before we called insert provisional on this cache associated with the stack we're now calling insert evaluation cache on the whole inference context. Well, the selection context, but and what that's going to do ignore this for a second that's going to go and inside the inference context, it's going to insert keyed by the parameter environment and the trait this time, which is correct, the depth, node and the result, and then we actually have this global cache too.

A

What's the difference, uh the evaluation cache is tied to things.

A

Basically, if that looks like something that is just true for everyone like u32, send or something we'll use the the big global cache and if it has inference variables or others or like generic parameters or something we'll use the uh inference context cache um this probably doesn't they don't they they sort of both need to exist, but not entirely. um I like choc's version of this better uh using canonicalization and stuff, and then this is the other part on completion. What does that do?

A

uh This is what I actually changed in this pr. So mostly uh what this does is. It goes through everything in the provisional cache that is covered by this cycle, basically and goes and puts it in the global cache, because now, like I said, bar and baz, we not only know that foo is true. We know that the things that we're dependent on foo are also true and here's. Here's what changed um in order to show what changed. I have to make a slightly more annoying example, uh and maybe to explain how this works better.

A

So this example had only one cycle, but the actual example from the bug is more like a depends on b depends on c. Well, we don't need to make it that complicated. A depends on b, which depends on a so now we have a cycle depends on c depends on d depends on c now we have another cycle and that's the key point. This cycle.

A

uh

A

um Sort of contained within this greater cycle right- um and I think, in the actual example of the code, like a also depends on like an e that depends on c. This doesn't really matter, but that could happen, um and so what we used to do in the old code was you kind of consider this all one big cycle?

A

um We would.

A

We would wind up uh we had for for the cash itself a reached depth.

A

There was the minimum of the reach depth of all of the provisional entries in the cache rather than having a per entry value, and so we said everything in this cache becomes true at that depth, um and that was okay, like that sounds like an approximation, a less good version of what we do now, but it actually led to incorrect results because there's one little detail, I didn't show you, which is this dot max, so we're not actually storing the result that was cached this okay result.

A

What we're storing when we go to the global result is sorry just having a thought. Is there a subtle, weird bug here? I think it's okay. uh What restoring is I have to think about it, though uh we're actually storing is the.

A

The max of that and the result from the main cache and there's this other little weird thing about failure. Let's ignore failure for a second and assume everything is true. The real problem here is there's two versions of true there's: okay and okay modular regions, um so things can be less true, but still true, where we say well, we had some region stuff to prove and we didn't. We didn't evaluate that, and so what was happening in the bug is, let's say, to prove e. This is ok, modulo regions.

A

Let's say it depended on c, and it also depended on this was the actual thing in sin depends on some type outliving tic static, which actually, we could just prove it's kind of, because, like there's, this is like literally a struct.

A

uh We don't need any fancy region logic to know that that that's true, but that's a very special case, um uh so we so we said okay well, this is okay, modulo regions, which makes e okay modular regions, which makes a okay modular regions, because a depends on all these things and then the idea is well.

A

For example, take b b depends on a.

C

So.

A

B, isn't really okay b is only as true as a is true, so so b is actually, even though we got an okay result. When we just looked at b in isolation, that's because we were assuming a was okay modular regions when, in fact, um because we were assuming a was okay, but if we re-ran this result to a fixed point, and we started with a being okay modular regions.

A

This time, instead of assuming a was okay, we would actually come back with okay, modular regions here makes sense, and so so what we're doing is we're kind of cutting instead of re-running to a fixed point, which is probably what we should do or is like the naive thing to do.

A

We're just doing the dot max here, because we know some stuff about our logic system and we know that it doesn't do anything besides. Propagate truth, up doesn't have negation in particular uh and so um yeah. So that's what's actually happening, and that's all fine, except for this part, because we would do that same thing to the result of c, which was also okay whoa. What just happened?

A

Okay, uh somehow I hit something, and so that means we would c and d were also okay. But if you look at those, even though they're sort of amongst it's a sub, even though it's like in this, it's a different strongly connected component, because from c you can't reach a so um so actually c isn't dependent on a and the fact that a is okay modular doesn't affect our c result.

A

It should just be okay, but because we didn't track that for each entry in the cache we couldn't recognize that, and so we wound up caching, ok modular region, and that was okay, because for the most part, that distinction doesn't really matter until in the incremental version or for whatever reason. When we restarted and we ran, we happened to compute c, without starting from a just starting from c, and in that case we would get the proper result, and so we would get a uh an assertion.

A

Failure recognizing that we actually got two different results without any change in the inputs.

A

So that's the bug and the fix is that now we store everything per depth, and that means when we get to c the reached depth of c is just going to be itself and so we're going to clear out everything.

A

At that point we haven't looked at e, yet keep that in mind, so we're going to clear out everything with a higher depth first number than c in the provisional cache, but not things with lower depth versus numbers. So when we get to see let's say contents of provisional cache when we finish with c we're going to have b is okay with a reach depth of zero, and we're going to have d is okay with a reach depth of zero, because in the course of proving c we had to prove d.

A

We haven't gotten to e. Yet so that's not going to be in the cache. Oh and I'm also going to add in the dfns just for fun. This is going to have from dfn1.

A

This is going to have from dfn2, which is the or 3, rather because this is dfn0123, um and so we're going to look for everything with a higher dfn than csdfn, which is 2. um and oh, and this reach depth is not zero. It's actually one uh and we're going to move it to the global cache and we're gonna max it with the result of c so we're gonna move.

B

C and d into.

A

The global cache.

B

That should be two right, not one. One is b.

A

No, this is this, is this is depth? That's confusing, there's no reason to use both the fn in depth, except that we do.

B

uh Oh great.

A

That's one of the things I refactored in my branch. We only use dfn, which.

C

I found to be.

A

Easier to think about.

B

Yeah, no that's confusing.

A

The fn has the advantage of not being reused so when you're gripping through logs and stuff, you don't get like weird results, um but otherwise I think you could use either one here, because it's but anyway we use different ones and it's confusing, but uh that's what we do so yeah one at this point is c for the depth right um so yeah. So that's the fix uh everything else just works. I think I didn't really change anything else in this branch. um The only problem is we're getting this assertion. Failure.

A

I don't understand. uh Let me just check. What's on my schedule? Oh right, okay, that's all right! I have a phone call to make other than that we're okay, um it's one of those things where anything that any business that doesn't open before. I start working, it's very hard for me to deal with my brain gets into rust and like it doesn't let go until like 7pm and then most pistons are closed uh yeah.

A

um So anyway, uh where were we right? The bug? So I don't know what the problem is. Let's take a look. It's an assertion. Failure. The problem is update, reach depth and maybe the assertion's just wrong. For some reason. uh I don't think so. um We're asserting that.

A

Yeah, that's weird: why is that? That does seem weird we're asserting that nobody ever calls? No one ever tells us to update our depth to something below us or newer than us.

B

That makes sense, you think.

A

I think it does right because if there's a cycle then either we're the start of the cycle, so it should be equal to us or it's older than us, or if it's newer than us, then it's not doesn't affect us. So why do we care um it's not actually harmful, like it may be that it's just getting cold and it's not harmful, but it's weird, um I'm wondering yeah. So, oh there's one other thing before we go on to this bug. I just want to mention one thing that the logic does do today.

A

I change this in my branch and I think it's right, though I have to completely convince myself if the result isn't is not okay or okay, modulo regions.

A

It clears everything on the cache that comes after it that every so, in other words, going through our whole example here, if a had turned out to be an error.

A

We would have cleared this provisional result and we would never move it to the global cache, so this dot max that's occurring here. I believe you could put an assert- and maybe I should that result.

A

This code should only ever execute in the case where the result we're maxing with is either okay or okay modular regions, because otherwise the cache should have been cleared. um I don't actually think that's necessary. I think it would be okay to like if, if the result was error, we could cache error, because it's not true and when.

C

We.

A

Evaluate it we're going to get an error, but.

B

Yeah.

A

What was your.

B

Reasoning for discarding error.

A

I don't know that's what I'm I'm a little. I would like to go back and ask myself. um I think I was not. I might have been a little nervous because it is certainly true that well basically, the question is, I think, it's similar to the dot max logic.

A

Like that's a shortcut, that's making an assumption, which is that if, if we found that that b is true, if a is true, if we knew that a was false, would we we're assuming we could never prove b, to be true right, which I think should be correct like?

A

But if you had.

A

If you could imagine that the code might do something different like say, try to evaluate a and if I don't know, then I'll go down one path, but if I know it's an error, I'll go down another path and like in particular the where clause winnowing and stuff, I wouldn't be totally shocked if there's some edge case where, if we were to run this to a fixed point, it would do something different.

A

uh So it makes me like mildly uncomfortable, um but that code in general just makes me mildly uncomfortable. uh I think that's a good example why that code is bad. um I if, if we had negation this all this logic gets a little more complicated, which is why well, we don't have negation in chalk either anymore, but like the old slg solver, maybe before you started hacking on. I can't remember.

B

I removed the negation.

A

This is why it used to have two: it used to have two things: positive reached depth effectively and negative reach depth, because it basically you have, you will have to do somewhat different things um where you're you're either saying b is true. If a is true or you're, saying, b is true: if a is false, that's different, um but um but we don't have that because we don't have nikki uh anyway. So let's look at this.

A

What happened to my terminal? It's like gone.

A

Okay, that's weird! um Oh there's like some anonymous terminals here or something very weird.

A

um

A

Just gonna get rid of that. Something weird is going on: let's try this instead rust back trace. So I think what I found was in order to reproduce this problem.

A

I had to do dist, so I think it dies when running rust, dock or something.

A

Which is always a good sign.

B

Yeah, I definitely run into that crosstalk does some unusual.

A

Things with the trade solver, which exercise some different paths. So I'm not that surprised uh right. So we've got some. I think what I would like to do is dump let's dump some state while we're here too.

A

This is going to generate a bunch of crap, isn't it I hope not? Let's find out, I had some fun cases of like two terabyte log files, while debugging the same thing, yeah.

B

I always do my best to like get an mcb and then.

A

It really makes life better.

B

Yeah.

A

The uh the nice trick that I was using with some success, but that is a little risky, is like piping. It through rip grep dash, see a thousand or something so you get find some string that you care about, and then you get a thousand lines before and after that string each time it appears.

A

But then you never quite know like when you try to find every occurrence of something or if it's not, that exact string. You don't quite know if it's in there or not yeah.

B

I think it depends. Usually I can get an mcbe and then I just like vlog freight selection, infer rusty middle just the big grapes.

A

Let's take a look here so we're getting this hit from evaluate trade, predicate site recursively, which probably.

A

Is here right?

A

That would be my guess, um like it's probably a provisional cash hit, and so what I'm wondering is, could it happen.

A

I feel like the there's something.

A

Okay, maybe I can see how this no. It feels like this shouldn't happen. This feels bad. So what I'm imagining could have happened is.

A

ah I think I know what could happen. Maybe this is an argument for switching to dfns, um which isn't that much work. uh I think what could be happening is: let's try to sketch it out um scott. Why are you not? Why are you doing that.

A

I don't understand what it's doing don't make a new terminal, no.

B

uh I don't know maybe try closing the terminal.

A

Let's close something.

A

um No, I guess all that stuff was that's fine, it doesn't matter um there. We go.

A

No.

B

Why.

A

Are you doing this to me also how big is kill me.

A

Pretty big, okay, it's not worth it we'll figure, something else out. uh What we'll do is this.

B

You could just winnow it to the trade select module.

A

Yeah that might help too.

A

um But also I should close this, maybe something gonna. Let me have. I think I just have to restart ps code.

A

It's very grumpy.

A

We'll worry about you later, uh so here's what I think is happening, even though I can't type to show you.

A

um I think that we are completing a provisional cache and then the thing that which was dependent on let's say something with one depth, and then we go to do other things within that which wind up making the depth higher, but we're not updating the cache entries.

A

If that makes sense, um yeah.

B

I think that makes sense.

A

If we use dfn.

A

I think it would.

B

Be the same problem.

A

And that's probably why I made one: that's probably why I had yeah. That's why I had one depth in the beginning, because I exactly this transitive thing I didn't want to deal with it. um I remember that now it's good. We should probably add a test for this uh yeah. That is not like yeah. I know good luck.

B

Minimizing it.

A

It's something very sensitive: it's possible.

B

We could add.

A

A test for this.

B

Surprised you were able to figure this out.

A

You should be able to make a test for this come on uh hold on the problem. With these tests is they're always so dependent on, like.

A

I don't know um I mean it's something like.

A

Tray a I guess, these have to be auto traits. Okay, it's something like struct.

A

A great hold on, let's show the graph we want. The graph we want is a depends on b depends on.

A

E or maybe just b depends on b.

A

And then b also depends on a and then that will make b have it or we probably need an intermediate node to make. It really do the right thing, so this would have a depth of one. This would have a depth of zero and now the overall result is a depth of zero right. um What we can do.

A

I actually don't. I don't particularly love the structure of this cache, because it's a it's a um hash map which is annoying because so much of what we want to do is dependent on the depth first numbers really um but like what we could very easily do is when we decide when we're done with b, and we see that we're going to insert our thing as provisional, we can also sweep everything with a higher depth.

A

First number: that's in the cache and update its like its depth should it's reached up should be the minimum of uh our reach depth. If that makes sense, you know um yeah, I'm trying to think if that's early enough or if we can have a problem where um you haven't yet left b, and it's already annoying that it's out of date.

A

I don't think so, because.

A

Basically, the reach depth of everything. That's in the cache.

A

Is always something that is still on the stack like in order to have a problem? It would have to be a depth of some node that was popped right. That's the problem, we're having that we popped b from the step back like we didn't complete the whole the whole. The assertion fails when we then go to process d and we find a provisional cache result for c with depth one um this problem.

A

This actually won't trigger this version, but to make the thing a little more convoluted, it should uh like you need, like another layer or something to make it depth to um which was annoying. But uh that's where we have the problem, and the problem is that it's referring to b but b was popped, but we maintain the invariant. If, if what we do is when we top b- and we see that b- isn't ready. Yet we go and update everybody's depth to b's depth.

A

It must be something lower than b, or else b would have been ready, and so we kind of maintained that invariant that the depth is always referring to some some parent on the stack which might be ourselves or which will never be. It will never be d because d, if there's some common ancestor and d, is a child of that, and at that point before d was pushed everything on the stack referred to a or above that make sense. um It does. It's true trust me.

B

Trust me.

A

It's fine. It's.

B

It sounds correct.

A

You can sort of see what I'm getting for. I hope yeah.

B

uh

A

Yeah, okay, so now I just have that's. The easiest fix is to do that, but I do I would like to have a test. It's gonna be annoying to make one though um I need like I need a. I need. The cache result to be depth. Two, oh well. Okay, so c has depth one. So if, if a.

A

If a just depends on c.

A

That do it.

A

I think that would do it, because what would happen is a will come along. A will find the provisional cache result.

A

C won't yet be on the stack.

A

So let's try it. I think this will work.

B

That looks right because it would go through b, update a with a depth of zero, go to c see it's step. One try to update a get some.

A

Garbage in the way to prevent it from prevent other things from freaking out uh c has to depend on b.

A

Or let's just do like no that'll work.

A

Of course, that worked fine.

B

But you don't depend on c again from a right. It's only through good point.

A

Still not good enough, why b depends on c and a.

A

um I don't know: let's look at the logs, why is this so smart?

A

It could be that it's not even evaluating this. It might not even be going down this path. Actually, it's kind of annoying it's hard to make it. It's not always easy to make it do an evaluation. uh Yeah.

B

That's at least with chalk right. You can just tell it what you want it to do.

A

Trying to think what's a way to force it to do an evaluation. It will do it if there's two work, if there's two options that might apply um and it needs to narrow it down so like we could do.

A

Implement for all t, nitrate, no for all t that are a my trait for t and.

B

Not sure that'll work because t implements a doesn't make sense. It's destruct.

A

Oh you're, right that does not work uh send, is what I.

A

Wanted, of course, that doesn't work well.

A

I don't know.

B

I mean, I don't know you could restrict t to. I don't know.

A

It's not gonna work because it's not gonna unify.

A

What happens if I do this?

A

No okay, I don't know just fix it.

B

Stop being so, smart.

A

Stop being smart, all right, we'll try to just fix the bug. uh What we really need is yeah, so insert provisional.

B

I feel like update the when you update the dfn or the reach depth. That should just if it's greater just ignore it right, because.

A

Well, I'm that doesn't feel right to me because it actually does depend on like if b depends on. If c depends on a like to go back to our example. I thought about that. But I think that's wrong, because c really does depend on a here right and if we, if we just ignored the depth, we don't know that we don't realize that there's actually a dependency between processing c and the thing at depth zero, and so we might incorrectly assume that some parent node is complete.

B

Wait I'm confused, so we so we're at the point that we finish processing b, so the root depth of a is going to be zero. We go to try to process c now we have. We see that that's the root depth of one. We want to update a to b, at least um older than one, but it's.

A

Already, zero right, this doesn't show the problem. The problem would be if we suppose that we add some more layers in here.

A

Don't don't make me write all the layers out suppose that we had another layer. I guess the layers have to be.

A

Here.

A

Oh, I hate this.

A

Suppose that this was depth one right now we'll get a reach depth of two right and we would go up, and this has reached depth one because it started that way, and this has reached up zero.

A

Now, my my concern is: we walk up the stack, we say ah well, that's inside of us, so we don't have to update or reach depth of one okay and then, but the problem is now we might actually cache this result in the global cache when in fact it does depend on a because c depends on b, which depends on a so. It's actually wrong.

B

Yeah, I see.

A

um I think the right result I'm trying to decide the most. I think that there's a number of times you could do this, but the bottom.

C

Line is you have to.

A

Like we could use, we could what we could do is um we could do the? What do you call it union find algorithm like union? Find is probably actually the easiest way to do this, which is to say that we, you know, we say: okay, wait. What was the? What was the minimum dfn?

A

If we used dfns and stuff, we could poke back up and get union find that would be like that maximally efficient. We would say we would just never forget that. As the end result, we'd have. The dfn for c would be. Okay well c depended on b, and then we would we would unify b with a and then we would say uh we found c, let's, let's refresh to whatever's the transient thing, so that makes sense. um Yeah wait.

B

I feel like using union, find why.

A

Did.

B

Why did b not get updated to zero here? Oh.

A

It will, it will b will get updated to zero, but that's not the problem. The problem is here. This is reach. Depth equals one, because at the time when b gets.

B

But I mean, oh, I see what you mean. Yeah because c depends on b depends on a.

A

Right so d union five would be like the laziest thing, but I think just eagerly updating them. When we pop b is the easier thing and probably more correct, or I don't know whether it's more efficient they're, probably both fine, um that's what I'm going to do.

A

It's not hard. It's just annoying. um Basically, I think what you would do is when you insert a provisional entry.

A

You want to say everything everything with a dfn greater than my dfn has to have. It has to have the minimum of its depth and my depth because that's stuff that was added after I started, and it's all now dependent on anything that I'm dependent on.

B

Yeah, that sounds like it: it'll work.

A

It will work and I do have to drop off now because I have another call, but we've at least I think we covered everything I wish I had a test for this. ah It's so annoying there should, we should add some rusty attribute or something that lets us.

B

Be clever and tell girls.

A

No that lets us do like what we can do in shock. Yeah rusty, evaluate predicate a my trait or something you know. uh The annoying thing is, I also couldn't. I could not convince that standalone test to reproduce for me in in any way partially, because I don't have this like. If I had this capability, I think we could do it, but I couldn't like trigger the evaluates in the right order without turning off debug assertions and turning on other things, yeah.

B

I mean conceptually, I understand, what's going on, I will have to go back and like look through your exact changes and like double check that everything lines up.

A

Yeah, oh it's good. I mean it's good for me to talk it out and through some depth I've. I didn't encounter any points where I was like. Oh wait a minute. So that's a good sign.

A

All right see you later.

B

Thanks bye.
youtube image
From YouTube: 2021-05-12 Trait Evaluation Caching (PR #85186)

Description

Niko and Jack Huey walking through how caching of trait evaluation works. The context is explaining PR #85186.