Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feature to use unbounded weights #1081

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
DDlog, which will crash DDlog programs at runtime if they overflow the
weights attached to data values. This may be preferable to generating
incorrect results.
- Rust compilation option `unbounded_weights` for the code generated by
DDlog which will never crash DDlog programs at runtime but may be slower.

## [0.48.2] - Sep 13, 2021

Expand Down
9 changes: 8 additions & 1 deletion doc/tutorial/tutorial.md
Original file line number Diff line number Diff line change
Expand Up @@ -3797,12 +3797,19 @@ Weight overflow in turns leads to silent wrong results at runtime [bug
878](https://github.com/vmware/differential-datalog/issues/878).

To mitigate this problem, the generated Rust code can be compiled with
the a feature named `checked_weights`. This causes programs that
a feature named `checked_weights`. This causes programs that
overflow the weights to crash with a Rust `panic` at runtime instead
of producing incorrect results. This can be done e.g., by compiling
the result produced by the ddlog compiler with a command line like
`cargo build --release --features=checked_weights`.

Alternatively, the generated Rust code can be compiled with a feature
named `unbounded_weights`. This may cause the program to execute
slower and use more memory, but the program will never produce
incorrect results. This can be done e.g., by compiling
the result produced by the ddlog compiler with a command line like
`cargo build --release --features=unbounded_weights`.

## Profiling

DDlog's profiling features are designed to help the programmer identify
Expand Down
6 changes: 3 additions & 3 deletions lib/ddlog_std.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1264,7 +1264,7 @@ impl<K: Clone, V: Clone> Clone for Group<K, V> {
key: key.clone(),
group: group
.iter()
.map(|(v, w)| tuple2(project(v).clone(), i64::from(*w) as DDWeight))
.map(|(v, w)| tuple2(project(v).clone(), i64::from(w.clone()) as DDWeight))
.collect(),
},
GroupEnum::ByVal { key, group } => GroupEnum::ByVal {
Expand Down Expand Up @@ -1435,7 +1435,7 @@ impl<'a, V: Clone> Iterator for GroupIter<'a, V> {
match self {
GroupIter::ByRef { iter, project } => match iter.next() {
None => None,
Some((x, w)) => Some(tuple2(project(x).clone(), i64::from(*w) as DDWeight)),
Some((x, w)) => Some(tuple2(project(x).clone(), i64::from(w.clone()) as DDWeight)),
},
GroupIter::ByVal { iter } => match iter.next() {
None => None,
Expand Down Expand Up @@ -1531,7 +1531,7 @@ impl<V: Clone> Iterator for GroupIntoIter<V> {
match self {
GroupIntoIter::ByRef { iter, project } => match iter.next() {
None => None,
Some((x, w)) => Some(tuple2(project(x).clone(), i64::from(*w) as DDWeight)),
Some((x, w)) => Some(tuple2(project(x).clone(), i64::from(w.clone()) as DDWeight)),
},
GroupIntoIter::ByVal { iter } => match iter.next() {
None => None,
Expand Down
5 changes: 2 additions & 3 deletions rust/ddlog_benches/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,9 @@ edition = "2018"
license = "MIT"

[features]
# Use the following to run with checked_weights:
# panic on weight overflow.
#default = ["benchmarks_ddlog/checked_weights"]
default = []
checked_weights = ["benchmarks_ddlog/checked_weights"]
unbounded_weights = ["benchmarks_ddlog/unbounded_weights"]

[dependencies]
criterion = "0.3.3"
Expand Down
6 changes: 3 additions & 3 deletions rust/ddlog_benches/Makefile.toml
Original file line number Diff line number Diff line change
Expand Up @@ -5,19 +5,19 @@ dependencies = ["bench-twitter", "bench-livejournal"]
# Runs the benchmark suite on the citations dataset
[tasks.bench-livejournal]
command = "cargo"
args = ["bench", "LiveJournal", "--bench", "live_journal"]
args = ["bench", "LiveJournal", "--bench", "live_journal", "${@}"]
dependencies = ["build-ddlog", "download-livejournal"]

# Runs the benchmark suite on the twitter dataset
[tasks.bench-twitter]
command = "cargo"
args = ["bench", "--bench", "twitter"]
args = ["bench", "--bench", "twitter", "${@}"]
dependencies = ["build-ddlog", "download-twitter"]

# Run twitter microbenchmarks only
[tasks.bench-twitter-micro]
command = "cargo"
args = ["bench", "twitter-micro", "--bench", "twitter"]
args = ["bench", "twitter-micro", "--bench", "twitter", "${@}"]
dependencies = ["build-ddlog", "download-twitter"]

# Runs `ddlog` to generate ddlog code
Expand Down
16 changes: 16 additions & 0 deletions rust/ddlog_benches/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,3 +30,19 @@ For info on writing benchmarks see the [criterion user guide] and the [criterion
[`cargo-make`]: https://github.com/sagiegurari/cargo-make
[criterion user guide]: https://bheisler.github.io/criterion.rs/book/index.html
[criterion docs]: https://docs.rs/criterion

### Supported features

The benchmarks can be run using checked_weights, which will cause a
Rust panic on weight overflow. This can be done by running:

```sh
cargo make benchmarks --features checked_weights
```

The benchmarks can be run using unbounded_weights, which will always
produce correct results, but may run slower. This can be done by running:

```sh
cargo make benchmarks --features unbounded_weights
```
Comment on lines +33 to +48
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Put this chunk above the links

1 change: 1 addition & 0 deletions rust/template/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ command-line = ["cmd_parser", "rustop"]
nested_ts_32 = ["differential_datalog/nested_ts_32"]
c_api = ["differential_datalog/c_api"]
checked_weights = ["differential_datalog/checked_weights"]
unbounded_weights = ["differential_datalog/unbounded_weights"]

[dependencies]
abomonation = "0.7"
Expand Down
2 changes: 2 additions & 0 deletions rust/template/differential_datalog/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ nested_ts_32 = []
c_api = []
# panic on weight overflow
checked_weights = []
# unbounded weights make the program slower but correct
unbounded_weights = []

[dependencies]
#differential-dataflow = "0.11.0"
Expand Down
4 changes: 3 additions & 1 deletion rust/template/differential_datalog/src/api/update_handler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -440,8 +440,10 @@ impl MTUpdateHandler for MTChainedUpdateHandler {
self.handlers.iter().map(|h| h.mt_update_cb()).collect();

Arc::new(move |relid, v, w| {
// not all weight implementations support copy
#[allow(clippy::clone_on_copy)]
for cb in cbs.iter() {
cb(relid, v, w);
cb(relid, v, w.clone());
}
})
}
Expand Down
Loading