feature branch: zsharp

[kwantam]

This is a draft PR for the zsharp branch. Still wip, not ready to merge, etc etc etc.

Please drop zsharp-specific issues in this thread.

closes #3
closes #23

[kwantam]

@alex-ozdemir I think this is getting to the point where we can think about merging it. This will also avoid continuing breakage as the branches evolve away from one another.

I've just rebased onto master, but I haven't gone through all the testing yet. Probably have to do some CI fixes before we can merge, etc. Worth having a quick chat about strategy?

[alex-ozdemir]

I agree: better to merge sooner than later. Re: strategy talk: what did you have in mind? I'm free in a few hours if you want to do a call, or we can discuss it here.

…

On Sun, Jan 30, 2022 at 11:19 AM Riad S. Wahby ***@***.***> wrote: @alex-ozdemir <https://github.com/alex-ozdemir> I think this is getting to the point where we can think about merging it. This will also avoid continuing breakage as the branches evolve away from one another. I've just rebased onto master, but I haven't gone through all the testing yet. Probably have to do some CI fixes before we can merge, etc. Worth having a quick chat about strategy? — Reply to this email directly, view it on GitHub <#30 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABMKJ5W2QIH66S53QGNISUDUYWFL7ANCNFSM5J6QIQUA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you were mentioned.Message ID: ***@***.***>

[kwantam]

On second thought, let me at least get CI passing again and then we can figure out if there are other things before reviewing and merging. I'll ping you again later this week.

[alex-ozdemir]

Sounds good.

…

On Sun, Jan 30, 2022 at 6:06 PM Riad S. Wahby ***@***.***> wrote: On second thought, let me at least get CI passing again and then we can figure out if there are other things before reviewing and merging. I'll ping you again later this week. — Reply to this email directly, view it on GitHub <#30 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABMKJ5RQY52LM562EL5OUUDUYXVBBANCNFSM5J6QIQUA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you were mentioned.Message ID: ***@***.***>

[kwantam]

Ah, one thing I've been looking at is avoiding runaway memory consumption. Things like the constant folding cache are an issue here. As an experiment, I've made the cfold cache bounded with an LRU eviction policy (though if the cache is too small this ends up triggering quadratic behavior, so it's not a slam-dunk).

I'm guessing we may eventually want the same for the type cache, but I notice that it's using FxHashMap rather than what's implemented in hashconsing. Is there a reason to prefer this? (I see also that it's a map from weak pointers rather than strong pointers, but that seems orthogonal to the hashing strategy unless I'm missing something). Put another way: would it be possible to standardize on one hashing approach, or do these really need to be different? (And if so: can we document why in the code?)

[alex-ozdemir]

Huh. I'd like to know more about the kinds of memory problems created by the constant folding cache. I'm not sure that dynamically evicting items is the right fix.

Re: hash tables: I guess there is a little heterogeneity. The TERM and TERM_TYPES tables both use fxhash, and the TermMap and TermSet types use hashconsing. These don't need to be different---we could standardize. Is there a particular benefit to doing so? Too my knowledge, all of our hash tables are based on the hash-consing unique ID (when possible), even if the hash they apply to that ID is a bit different.

Edit: if uniformity is the only benefit, that's enough benefit for me---I ask because I want to know if there is another problem with the current set-up.

[kwantam]

Well, the fundamental issue is that the constant folding cache has unbounded size (its key type is Term, not TTerm). When interpreting, this means that a long enough execution runs out of memory.

I kind of lied when I said it was a simple LRU eviction policy. The policy I'm playing with now is: the cache is unbounded during any particular invocation of fold_cache, but after the outermost fold_cache call returns the cache gets pruned to some maximum number of entries (which ends up dropping a lot of heap allocated intermediate terms). Probably the number of entries should be dynamically determined, but for now 64k seems to work.

The TERM and TERM_TYPES tables also grow in an unbounded way. (I'm experimenting with garbage collection heuristics.) This causes both massive slowdowns (because of repeated re-allocations of the TERM and TERM_TYPES backing stores) and huge memory use---easily tens of gigs.

[alex-ozdemir]

I understand. Clearing between folds sounds like the right approach.

I'm glad you're looking into GC for terms. I'm sure you've already found my starting point

[kwantam]

OK, 5e85e56 takes a first cut at automatically invoking garbage collection.

Here's how it works: the term and type caches track how large they were after the last garbage collection. When ir::term::maybe_garbage_collect is called, each cache is collected only if its size exceeds some threshold based on the prior collected size. To avoid getting into a situation where the cache is never collected, the threshold decays over time, which forces a collection every once in a while.

In the zsharp front-end, maybe_garbage_collect is invoked when returning from a function call---sometimes. Only sometimes, because invoking ir::term::maybe_garbage_collect after every function call is too expensive.

In particular, there's a function call depth threshold; when returning from a call shallower than the threshold, ir::term::maybe_garbage_collect gets called. The depth threshold is dynamically determined: if ir::term::maybe_garbage_collect actually results in a collection event, then the depth threshold is increased (i.e., more collection events). Otherwise, the threshold is decreased (fewer collections). Once again, there's a bias in the threshold so that over time a collection will be forced. This helps to keep the feedback loop searching for the "right" depth.

I've tweaked the parameters of the various thresholds and leaky buckets based on one or two big example programs. The garbage collection overhead is nontrivial for small programs, but easily pays for itself in terms of avoiding massive cache reallocations and memory usage blow-up in big programs.

I think all of this could be incorporated into the IR itself, likely keying on circify's function return machinery. That will have to wait until we pull the interpreter-for-"free" down into the IR, though.

[kwantam]

@alex-ozdemir there seems to have been a brokenness in the obliv pass that more aggresive constant folding revealed. I think this code is wrong:

circ/src/ir/opt/mem/obliv.rs

Lines 100 to 108 in 09c9f03

	Op::Select => {
	let a = &term.cs[0];
	let i = &term.cs[1];
	if let Op::Const(_) = i.op {
	false
	} else {
	self.mark(a)
	}
	}

By this logic and the definition of mark(), if the index is non-constant then the array gets marked non-oblivious only if the array itself is non-constant. But this seems wrong, and indeed it ends up causing an issue: when compiling examples/C/mpc/unit_tests/array_tests/2pc_array_index.c with commit 00684d9, after constant folding the array is constant but the index is not, which causes the obliv pass to panic in obliv::get_const on the (non-const) index term. You can reproduce this by building circ on that commit and running something like

CARGO_MANIFEST_DIR=~/git/github.com/circ RUST_BACKTRACE=1 RUST_LOG=debug circ --parties 2 ./examples/C/mpc/unit_tests/array_tests/2pc_array_index.c mpc --cost-model hycc

Commit 81a0757 fixes this and recovers correct behavior, by marking both the array and the parent term if the index is non-const. At least, I think this is right, based on what's going on in the corresponding Op::Store code a few lines above.

Can you double check me on this?

[kwantam]

Ugh, my mistake. That still doesn't fix the issue. I'm not sure why yet, but I'll look into it. Not obvious to me why const arrays shouldn't be marked non-oblivious, though.

[kwantam]

Yeah, this seems wrong:

circ/src/ir/opt/mem/obliv.rs

Lines 219 to 228 in 81a0757

	Op::Select => {
	if self.should_replace(&orig.cs[0]) {
	let mut cs = get_cs();
	debug_assert_eq!(cs.len(), 2);
	let k_const = get_const(&cs.pop().unwrap());
	Some(term(Op::Field(k_const), cs))
	} else {
	None
	}
	}

This tries to replace Op::Select if the array is marked oblivious, even if the Op::Select is marked non-oblivious. It seems like the right thing is to require both orig and orig.cs[0] to be oblivious, no?

EDIT: in this case, should Op::Store also require both orig and orig.cs[0] to be marked oblivious? I think maybe yes...?

[alex-ozdemir]

Oof! Yes, that was a bug. Thanks for looking into it, and for the patch.

Your fix has the right idea here: we should include non-oblivious selects in the non-oblivious set (even though they may not be arrays!) so that we can easily tell whether to replace them. Looking at the non-oblivious-ness of their parent array isn't sufficient b/c we never flag constant arrays as non-oblivious. I added a bit more code to your patch to reliably flag non-oblivious selects.

I also documented a bunch.

I still suspect that some of our array passes have bugs. The problem is that we really want to treat functional arrays as RAM, but that is surprisingly hard. It might be a fun Coq project to:

1. model a term IR, with functional arrays (like ours!).
2. model a RAM-augmented term IR, with conditional stores and reads
3. write a converter
4. prove that it works

I'm sure that we'd find bugs, and fix our algorithms. I'd sleep better at night too :). It might take some work to convince others that this project matters, but perhaps we could find a way.

[alex-ozdemir]

Since this script appears to be going into CI, we probably want to return a non-zero code on failure.

Sorry for the drive by comment. I just noticed this while testing.

[kwantam]

I still suspect that some of our array passes have bugs. The problem is that we really want to treat functional arrays as RAM, but that is surprisingly hard. It might be a fun Coq project to:

1. model a term IR, with functional arrays (like ours!).

2. model a RAM-augmented term IR, with conditional stores and reads

3. write a converter

4. prove that it works

This is a great idea. I'll add it to the TODO file!

[kwantam]

Thoughts on merging? Want to take a bit more time to review first?

[alex-ozdemir]

Yeah, I think we can merge soon. I’ll do a read-through this evening.

[alex-ozdemir]

Looks good to me. Feel free to squash & merge.

I left a few comments double-checking things.

Also, I benchmarked the (old) zokrates test script against the old and new binaries, to check for regression. Results:

Before:
Benchmark #1: ./scripts/zokrates_test.zsh
  Time (mean ± σ):      2.325 s ±  0.064 s    [User: 3.879 s, System: 0.379 s]
  Range (min … max):    2.211 s …  2.424 s    10 runs

After:
Benchmark #1: ./scripts/zokrates_test.zsh
  Time (mean ± σ):      2.576 s ±  0.069 s    [User: 4.123 s, System: 0.386 s]
  Range (min … max):    2.471 s …  2.707 s    10 runs

This looks fine to me. I'd expect a small slowdown given the new machinery we need for Z#.