Skip to content

Commit

Permalink
Merge latest changes from master
Browse files Browse the repository at this point in the history
Signed-off-by: Thane Thomson <[email protected]>
  • Loading branch information
thanethomson committed Nov 25, 2020
2 parents 62cbdca + b159940 commit 281a0a8
Show file tree
Hide file tree
Showing 15 changed files with 28 additions and 42 deletions.
8 changes: 0 additions & 8 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,5 @@
## Unreleased

### BREAKING CHANGES

- `[tendermint-rpc, tendermint-light-client]` Upgrade Tokio to version 0.3.0 ([#683])
- Upgrade `hyper` to `v0.14-dev`
- Upgrade `async-tungstenite` to `v0.10`

### IMPROVEMENTS:

- `[light-client]` Only require Tokio when `rpc-client` feature is enabled ([#425])
Expand All @@ -14,7 +8,6 @@

[#425]: https://github.com/informalsystems/tendermint-rs/issues/425
[#646]: https://github.com/informalsystems/tendermint-rs/pull/646
[#683]: https://github.com/informalsystems/tendermint-rs/issues/683


## v0.17.0-rc3
Expand Down Expand Up @@ -46,7 +39,6 @@ serialization infrastructure.
[#667]: https://github.com/informalsystems/tendermint-rs/issues/667
[#672]: https://github.com/informalsystems/tendermint-rs/pull/672
[#679]: https://github.com/informalsystems/tendermint-rs/issues/679
[#672]: https://github.com/informalsystems/tendermint-rs/pull/672

## v0.17.0-rc2

Expand Down
2 changes: 1 addition & 1 deletion light-client/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ serde_derive = "1.0.106"
sled = "0.34.3"
static_assertions = "1.1.0"
thiserror = "1.0.15"
tokio = { version = "0.3", features = ["rt"], optional = true }
tokio = { version = "0.2", optional = true }

[dev-dependencies]
tendermint-testgen = { path = "../testgen"}
Expand Down
3 changes: 2 additions & 1 deletion light-client/src/utils/block_on.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,8 @@ where
F::Output: Send,
{
std::thread::spawn(move || {
let rt = tokio::runtime::Builder::new_current_thread()
let mut rt = tokio::runtime::Builder::new()
.basic_scheduler()
.enable_all()
.build()
.map_err(|_| IoError::Runtime)?;
Expand Down
8 changes: 4 additions & 4 deletions light-client/tests/support/model_based/Abstract.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

We present our instantiation of model-based testing (MBT) using the TLA+ modeling language and the Apalache model checker. In our work we have created the infrastructure that facilitates model-based testing, and makes it appealing and beneficial for software developers to apply in their everyday development practice -- much more so than the standard integration testing with manually written tests that we've employed previously.

Our model-based testing procedure finds its rightful place in the verification-driven development process (VDD) we apply at Informal Systems. More concretely, we use it as an alternative approach to integration testing of the implementation in the Rust programming language of the fault-tolerant distributed consensus protocol named Tendermint. In the VDD process, we start with the semi-formal English language description of the protocol, which is then formally specified in TLA+, and verified by our Apalache model checker. The TLA+ specification is used as a reference model for clarifying misunderstanding both at the English language level, and at the level of the concrete implementation in Rust. Model-based tests are expressed in pure TLA+, and respresent simple assertions on the computation history the user wants to examine. Consider the model-based test below:
Our model-based testing procedure finds its rightful place in the verification-driven development process (VDD) we apply at Informal Systems. More concretely, we use it as an alternative approach to integration testing of the implementation in the Rust programming language of the fault-tolerant distributed consensus protocol named Tendermint. In the VDD process, we start with the semi-formal English language description of the protocol, which is then formally specified in TLA+, and verified by our Apalache model checker. The TLA+ specification is used as a reference model for clarifying misunderstanding both at the English language level, and at the level of the concrete implementation in Rust. Model-based tests are expressed in pure TLA+, and represent simple assertions on the computation history the user wants to examine. Consider the model-based test below:

```tla+
Test2NoSuccess ==
Expand All @@ -18,16 +18,16 @@ This is the model-based test of the Tendermint LightClient sub-protocol, which i

In our presentation we would like to convey three main messages on model-based testing, which we describe below.

## Model-based testing with TLA+ is easy to understand, and can be sucessfully appllied in the industry to provide correctness guarantees for real-world software.
## Model-based testing with TLA+ is easy to understand, and can be successfully applied in the industry to provide correctness guarantees for real-world software.

In our initial experience of implementing and applying MBT, we find quite appealing its simplicity for the end user, being it a researcher or a developer. The model-based tests are quite abstract and concise; they can precisely describe what behavior needs to be tested. At the same time, in sharp contrast to standard integration tests, they leave a lot of details unspecified. An important feature of MBT is that these missing details will be instantiated in different ways with each run of the model-based test; moreover, this behavior can be easily employed to _exhaustively_ test all scenarios falling under the abstract test. In the above example, the intermediate results are only restricted to be unsuccessful, but concrete verification errors are left open. And the model checker will indeed instantiate for each run different combinations of failures: due to the blockchain block falling out of the trusting period, not enough trust in the validator set, signature validation errors, etc.

One of the main reasons for the Tendermint modeling and model-based testing being successfully implemented and accepted within our teams is the rich syntax and sematics of the TLA+ language. TLA+ allowed us to concisely model the complex aspects of the Tendermint protocol, as well as to express correctness properties and tests about it. In particular, even for developers without a prior exposure to TLA+, following the models written by our researchers has helped to clarify the protocol abstractions before diving into the implementation, thus avoiding the painful experience and countless hours of correcting them when the implementation is already done.
One of the main reasons for the Tendermint modeling and model-based testing being successfully implemented and accepted within our teams is the rich syntax and semantics of the TLA+ language. TLA+ allowed us to concisely model the complex aspects of the Tendermint protocol, as well as to express correctness properties and tests about it. In particular, even for developers without a prior exposure to TLA+, following the models written by our researchers has helped to clarify the protocol abstractions before diving into the implementation, thus avoiding the painful experience and countless hours of correcting them when the implementation is already done.


## Substantial infrastructure is necessary for model-based testing, but the complexity is reasonable.

Some infrastructure naturally needs to be implemented in order to apply MBT. The good news is that a lot of that infrastructure is reusable: some for different components of the same product, some for different products or even different companies. Within our first MBT project we have implemented the following infrastructure components, highlighed in the figure:
Some infrastructure naturally needs to be implemented in order to apply MBT. The good news is that a lot of that infrastructure is reusable: some for different components of the same product, some for different products or even different companies. Within our first MBT project we have implemented the following infrastructure components, highlighted in the figure:

* Apalache model checker extension for providing JSON input/output (reusable globally);
* JSON Artifact Translator (Jsonatr), which, with the help of a transformation specification, maps an abstract counterexample produced by the model checker, into the concrete integration test (the tool reusable globally, the transformation spec -- for a specific product);
Expand Down
4 changes: 2 additions & 2 deletions light-client/tests/support/model_based/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ So, for the model-based test to run, the programs `apalache-mc`, `jsonatr`,
`tendermint-testgen`, and `timeout`
should be present in your `PATH`. The easiest way to run Apalache is by
[using a Docker image](https://github.com/informalsystems/apalache/blob/unstable/docs/manual.md#useDocker);
to run the latter two you need to locally clone the repositories, and then,
to run `jsonatr` and `tendermint-testgen` you need to locally clone the repositories, and then,
after building them, just add their `target/debug` directories into your `PATH`.
If any of the programs is not found, execution of a model-based test will be skipped.

Expand Down Expand Up @@ -75,4 +75,4 @@ and temporarily remove/rename other test batches (files or directories starting
files into the [single_step](single_step) directory.
4. Next time you run `cargo test` these static tests will be picked up and executed automatically.



2 changes: 1 addition & 1 deletion light-node/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ tendermint = { version = "0.17.0-rc3", path = "../tendermint" }
tendermint-light-client = { version = "0.17.0-rc3", path = "../light-client" }
tendermint-rpc = { version = "0.17.0-rc3", path = "../rpc", features = [ "http-client" ] }
thiserror = "1.0"
tokio = { version = "0.3", features = ["full"] }
tokio = { version = "0.2", features = ["full"] }

[dependencies.abscissa_core]
version = "0.5.0"
Expand Down
4 changes: 2 additions & 2 deletions rpc-probe/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ description = """
all-features = true

[dependencies]
async-tungstenite = { version = "0.10", features = [ "tokio-runtime" ] }
async-tungstenite = { version = "0.9", features = [ "tokio-runtime" ] }
futures = "0.3"
getrandom = "0.1"
log = "0.4"
Expand All @@ -27,5 +27,5 @@ simple_logger = "1.11"
structopt = "0.3"
subtle-encoding = "0.5.1"
thiserror = "1.0"
tokio = { version = "0.3", features = [ "full" ] }
tokio = { version = "0.2", features = [ "full" ] }
uuid = "0.8"
4 changes: 2 additions & 2 deletions rpc-probe/src/error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ impl From<async_tungstenite::tungstenite::Error> for Error {
}
}

impl From<tokio::time::error::Elapsed> for Error {
fn from(e: tokio::time::error::Elapsed) -> Self {
impl From<tokio::time::Elapsed> for Error {
fn from(e: tokio::time::Elapsed) -> Self {
Self::Timeout(e.to_string())
}
}
Expand Down
4 changes: 2 additions & 2 deletions rpc-probe/src/plan.rs
Original file line number Diff line number Diff line change
Expand Up @@ -319,7 +319,7 @@ async fn execute_interaction(
info!("Executing interaction \"{}\"", inner_interaction.name);
if let Some(wait) = inner_interaction.pre_wait {
debug!("Sleeping for {} seconds", wait.as_secs_f64());
tokio::time::sleep(wait).await;
tokio::time::delay_for(wait).await;
}
if let Some(h) = inner_interaction.min_height {
debug!("Waiting for height {}", h);
Expand Down Expand Up @@ -419,7 +419,7 @@ async fn execute_subscription(
};
write_json(&config.in_path, name, &response_json).await?;

let mut timeout = tokio::time::sleep(subs.max_time);
let mut timeout = tokio::time::delay_for(subs.max_time);
let mut event_count = 0_usize;
loop {
tokio::select! {
Expand Down
13 changes: 3 additions & 10 deletions rpc/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -39,8 +39,6 @@ websocket-client = [
"async-trait",
"async-tungstenite",
"futures",
"tokio/rt",
"tokio/rt-multi-thread",
"tokio/fs",
"tokio/macros",
"tokio/stream",
Expand All @@ -63,16 +61,11 @@ uuid = { version = "0.8", default-features = false }
subtle-encoding = { version = "0.5", features = ["bech32-preview"] }

async-trait = { version = "0.1", optional = true }
async-tungstenite = { version = "0.10", features = ["tokio-runtime"], optional = true }
async-tungstenite = { version = "0.9", features = ["tokio-runtime"], optional = true }
futures = { version = "0.3", optional = true }
http = { version = "0.2", optional = true }
tokio = { version = "0.3", optional = true }
hyper = { version = "0.13", optional = true }
tokio = { version = "0.2", optional = true }
tracing = { version = "0.1", optional = true }
pin-project = "1.0.1"

[dependencies.hyper]
version = "0.14.0-dev"
git = "https://github.com/hyperium/hyper/"
rev = "121c33132c0950aaa422848cdc43f6691ddf5785"
features = ["tcp", "client", "http1" ]
optional = true
2 changes: 1 addition & 1 deletion rpc/src/client/transport/http.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
use crate::client::transport::utils::get_tcp_host_port;
use crate::{Client, Response, Result, SimpleRequest};
use async_trait::async_trait;
use hyper::body::Buf;
use bytes::buf::ext::BufExt;
use hyper::header;
use tendermint::net;

Expand Down
4 changes: 2 additions & 2 deletions rpc/src/client/transport/router.rs
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ mod test {
}

async fn must_recv<T>(ch: &mut ChannelRx<T>, timeout_ms: u64) -> T {
let mut delay = time::sleep(Duration::from_millis(timeout_ms));
let mut delay = time::delay_for(Duration::from_millis(timeout_ms));
tokio::select! {
_ = &mut delay, if !delay.is_elapsed() => panic!("timed out waiting for recv"),
Some(v) = ch.recv() => v,
Expand All @@ -136,7 +136,7 @@ mod test {
where
T: std::fmt::Debug,
{
let mut delay = time::sleep(Duration::from_millis(timeout_ms));
let mut delay = time::delay_for(Duration::from_millis(timeout_ms));
tokio::select! {
_ = &mut delay, if !delay.is_elapsed() => (),
Some(v) = ch.recv() => panic!("got unexpected result from channel: {:?}", v),
Expand Down
2 changes: 1 addition & 1 deletion rpc/src/client/transport/websocket.rs
Original file line number Diff line number Diff line change
Expand Up @@ -301,7 +301,7 @@ impl WebSocketClientDriver {
pub async fn run(mut self) -> Result<()> {
let mut ping_interval =
tokio::time::interval_at(Instant::now().add(PING_INTERVAL), PING_INTERVAL);
let mut recv_timeout = tokio::time::sleep(PING_INTERVAL);
let mut recv_timeout = tokio::time::delay_for(PING_INTERVAL);
loop {
tokio::select! {
Some(res) = self.stream.next() => match res {
Expand Down
4 changes: 2 additions & 2 deletions tendermint/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,8 @@ k256 = { version = "0.5", optional = true, features = ["ecdsa"] }
ripemd160 = { version = "0.9", optional = true }

[dev-dependencies]
tendermint-rpc = { path = "../rpc", features = ["http-client", "websocket-client"] }
tokio = { version = "0.3", features = ["macros"] }
tendermint-rpc = { path = "../rpc", features = [ "http-client", "websocket-client" ] }
tokio = { version = "0.2", features = [ "macros" ] }

[features]
secp256k1 = ["k256", "ripemd160"]
6 changes: 3 additions & 3 deletions tendermint/tests/integration.rs
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@ mod rpc {
let mut cur_tx_id = 0_u32;

while !expected_tx_values.is_empty() {
let mut delay = tokio::time::sleep(Duration::from_secs(3));
let mut delay = tokio::time::delay_for(Duration::from_secs(3));
tokio::select! {
Some(res) = subs.next() => {
let ev = res.unwrap();
Expand Down Expand Up @@ -311,7 +311,7 @@ mod rpc {
.broadcast_tx_async(Transaction::from(tx.into_bytes()))
.await
.unwrap();
tokio::time::sleep(Duration::from_millis(100)).await;
tokio::time::delay_for(Duration::from_millis(100)).await;
}
});

Expand All @@ -324,7 +324,7 @@ mod rpc {
);

while expected_new_blocks > 0 && !expected_tx_values.is_empty() {
let mut timeout = tokio::time::sleep(Duration::from_secs(3));
let mut timeout = tokio::time::delay_for(Duration::from_secs(3));
tokio::select! {
Some(res) = combined_subs.next() => {
let ev: Event = res.unwrap();
Expand Down

0 comments on commit 281a0a8

Please sign in to comment.