[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Mon, 1 Feb 2016 08:11:00 -0800 (PST)

Hi.

How would I go about checking that a system where certain actions taking place at some non-deterministic interleaving (let's call it an asynchronous system) is "essentially identical" -- i.e. does not introduce any bugs additional bugs -- to a system where actions can only occur in a certain order (let's call it the synchronous system)? Obviously, the asynchronous system implements the synchronous one, but I'd like to check the other direction. I could specify them both and show that they both satisfy the set of invariants I've defined, but I'm looking for a stronger resemblance, which I can't quite formally define, a resemblance that means that *no *property on certain "externally observable" behavior, whether explicitly defined or not, could possibly be violated by the asynchronous system. I think what I'm looking for is a manual partial-order reduction, but I'm not quite clear on the formal definition of that, either (although I may need to look into that in more depth).

A bit more concretely, suppose I'm modeling a distributed system where one node may notice a change in another node's state, and at some later time it may notice another change, and I'd like to check whether that nondeterminism is any "worse" than noticing both changes at once (or in two consecutive transitions). If true, my hypothesis would make abstracting the system (i.e., the opposite of refinement) much easier.

Ron

**Follow-Ups**:**Re: [tlaplus] Invariance under transition order***From:*Stephan Merz

- Prev by Date:
**Choose and TLC** - Next by Date:
**Re: A refinement mapping using "callbacks"** - Previous by thread:
**Re: [tlaplus] Re: Choose and TLC** - Next by thread:
**Re: [tlaplus] Invariance under transition order** - Index(es):