forked from delta-io/delta-rs
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
tla+ spec for dynamodb lock (delta-io#182)
Spec is model checked without pause and crash. Adding crash and pause to the modeling requires enabling timer in the spec (i.e. setting TIME_TICK_UNIT > 0). This will fail the model check because lock with expiration cannot guarantee correctness without use of fencing token.
- Loading branch information
QP Hou
authored
Apr 13, 2021
1 parent
c670b2a
commit 033d690
Showing
7 changed files
with
781 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,2 +1,9 @@ | ||
| /target | ||
| *.sw* | ||
| tlaplus/*.toolbox/*_SnapShot_*/ | ||
| tlaplus/*.toolbox/*_SnapShot_*.launch | ||
| tlaplus/*.toolbox/*.tla.pmap | ||
| tlaplus/*.toolbox/*/*.out | ||
| tlaplus/*.toolbox/*/*.tla | ||
| tlaplus/*.toolbox/*/MC.cfg | ||
| tlaplus/*.toolbox/*/[0-9]*-[0-9]*-[0-9]*-[0-9]*-[0-9]*-[0-9]*/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,7 @@ | ||
| This folder contains TLA+ proofs for various subsystems of the project including: | ||
|
|
||
| * Distributed Dynamodb lock | ||
| * S3 multi-writer design | ||
|
|
||
| To model check these specs, you need to use [TLA+ | ||
| toolbox](https://lamport.azurewebsites.net/tla/toolbox.html). |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,24 @@ | ||
| <?xml version="1.0" encoding="UTF-8"?> | ||
| <projectDescription> | ||
| <name>dynamodblock</name> | ||
| <comment></comment> | ||
| <projects> | ||
| </projects> | ||
| <buildSpec> | ||
| <buildCommand> | ||
| <name>toolbox.builder.TLAParserBuilder</name> | ||
| <arguments> | ||
| </arguments> | ||
| </buildCommand> | ||
| </buildSpec> | ||
| <natures> | ||
| <nature>toolbox.natures.TLANature</nature> | ||
| </natures> | ||
| <linkedResources> | ||
| <link> | ||
| <name>dynamodblock.tla</name> | ||
| <type>1</type> | ||
| <locationURI>PARENT-1-PROJECT_LOC/dynamodblock.tla</locationURI> | ||
| </link> | ||
| </linkedResources> | ||
| </projectDescription> |
2 changes: 2 additions & 0 deletions
2
tlaplus/dynamodblock.toolbox/.settings/org.lamport.tla.toolbox.prefs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| ProjectRootFile=PARENT-1-PROJECT_LOC/dynamodblock.tla | ||
| eclipse.preferences.version=1 |
53 changes: 53 additions & 0 deletions
53
tlaplus/dynamodblock.toolbox/dynamodblock___fast_dev.launch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,53 @@ | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <stringAttribute key="TLCCmdLineParameters" value=""/> | ||
| <intAttribute key="collectCoverage" value="1"/> | ||
| <stringAttribute key="configurationName" value="fast_dev"/> | ||
| <booleanAttribute key="deferLiveness" value="true"/> | ||
| <intAttribute key="dfidDepth" value="100"/> | ||
| <booleanAttribute key="dfidMode" value="false"/> | ||
| <intAttribute key="distributedFPSetCount" value="0"/> | ||
| <stringAttribute key="distributedNetworkInterface" value="192.168.86.239"/> | ||
| <intAttribute key="distributedNodesCount" value="1"/> | ||
| <stringAttribute key="distributedTLC" value="off"/> | ||
| <stringAttribute key="distributedTLCVMArgs" value=""/> | ||
| <intAttribute key="fpBits" value="1"/> | ||
| <intAttribute key="fpIndex" value="89"/> | ||
| <booleanAttribute key="fpIndexRandom" value="true"/> | ||
| <intAttribute key="maxHeapSize" value="86"/> | ||
| <intAttribute key="maxSetSize" value="1000000"/> | ||
| <booleanAttribute key="mcMode" value="true"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value="Spec"/> | ||
| <intAttribute key="modelBehaviorSpecType" value="1"/> | ||
| <stringAttribute key="modelBehaviorVars" value="owner_, record_version_, local_record_version, re_upsert_err, cached_lock_lookup_time_, lock_owner, pc, local_counter, next_time_tick, active_writer, lock_released, record_version, lock_record_version, time_now, cached_lock_duration_, cached_lock_version, shared_counter, cached_lock_duration, local_count_value, stack, owner, cached_lock_lookup_time, lock_duration"/> | ||
| <stringAttribute key="modelComments" value=""/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"> | ||
| <listEntry value="1ConsistentCount"/> | ||
| </listAttribute> | ||
| <listAttribute key="modelCorrectnessProperties"> | ||
| <listEntry value="1Termination"/> | ||
| <listEntry value="0NoMissCount"/> | ||
| </listAttribute> | ||
| <intAttribute key="modelEditorOpenTabs" value="0"/> | ||
| <stringAttribute key="modelExpressionEval" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="NULL;;NULL;1;0"/> | ||
| <listEntry value="WRITERS;;{w1, w2, w3};1;0"/> | ||
| <listEntry value="LOOP_COUNT;;5;0;0"/> | ||
| <listEntry value="TIME_TICK_UNIT;;0;0;0"/> | ||
| </listAttribute> | ||
| <intAttribute key="modelVersion" value="20191005"/> | ||
| <intAttribute key="numberOfWorkers" value="12"/> | ||
| <booleanAttribute key="recover" value="false"/> | ||
| <stringAttribute key="result.mail.address" value=""/> | ||
| <intAttribute key="simuAril" value="-1"/> | ||
| <intAttribute key="simuDepth" value="100"/> | ||
| <intAttribute key="simuSeed" value="-1"/> | ||
| <stringAttribute key="specName" value="dynamodblock"/> | ||
| <stringAttribute key="tlcResourcesProfile" value="local custom"/> | ||
| <stringAttribute key="view" value=""/> | ||
| <booleanAttribute key="visualizeStateGraph" value="false"/> | ||
| </launchConfiguration> |
52 changes: 52 additions & 0 deletions
52
tlaplus/dynamodblock.toolbox/dynamodblock___full_tiimeless.launch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,52 @@ | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <stringAttribute key="TLCCmdLineParameters" value=""/> | ||
| <intAttribute key="collectCoverage" value="1"/> | ||
| <stringAttribute key="configurationName" value="full_tiimeless"/> | ||
| <booleanAttribute key="deferLiveness" value="true"/> | ||
| <intAttribute key="dfidDepth" value="100"/> | ||
| <booleanAttribute key="dfidMode" value="false"/> | ||
| <intAttribute key="distributedFPSetCount" value="0"/> | ||
| <stringAttribute key="distributedNetworkInterface" value="192.168.86.239"/> | ||
| <intAttribute key="distributedNodesCount" value="1"/> | ||
| <stringAttribute key="distributedTLC" value="off"/> | ||
| <stringAttribute key="distributedTLCVMArgs" value=""/> | ||
| <intAttribute key="fpBits" value="1"/> | ||
| <intAttribute key="fpIndex" value="1"/> | ||
| <booleanAttribute key="fpIndexRandom" value="true"/> | ||
| <intAttribute key="maxHeapSize" value="86"/> | ||
| <intAttribute key="maxSetSize" value="1000000"/> | ||
| <booleanAttribute key="mcMode" value="true"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value="Spec"/> | ||
| <intAttribute key="modelBehaviorSpecType" value="1"/> | ||
| <stringAttribute key="modelBehaviorVars" value="owner_, record_version_, local_record_version, re_upsert_err, cached_lock_lookup_time_, lock_owner, pc, local_counter, next_time_tick, active_writer, lock_released, record_version, lock_record_version, time_now, cached_lock_duration_, cached_lock_version, shared_counter, cached_lock_duration, local_count_value, stack, owner, cached_lock_lookup_time, lock_duration"/> | ||
| <stringAttribute key="modelComments" value=""/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"> | ||
| <listEntry value="1ConsistentCount"/> | ||
| </listAttribute> | ||
| <listAttribute key="modelCorrectnessProperties"> | ||
| <listEntry value="1Termination"/> | ||
| <listEntry value="1NoMissCount"/> | ||
| </listAttribute> | ||
| <intAttribute key="modelEditorOpenTabs" value="4"/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="WRITERS;;{w1, w2, w3};1;0"/> | ||
| <listEntry value="TIME_TICK_UNIT;;0;0;0"/> | ||
| <listEntry value="NULL;;NULL;1;0"/> | ||
| <listEntry value="LOOP_COUNT;;10;0;0"/> | ||
| </listAttribute> | ||
| <intAttribute key="modelVersion" value="20191005"/> | ||
| <intAttribute key="numberOfWorkers" value="12"/> | ||
| <booleanAttribute key="recover" value="false"/> | ||
| <stringAttribute key="result.mail.address" value=""/> | ||
| <intAttribute key="simuAril" value="-1"/> | ||
| <intAttribute key="simuDepth" value="100"/> | ||
| <intAttribute key="simuSeed" value="-1"/> | ||
| <stringAttribute key="specName" value="dynamodblock"/> | ||
| <stringAttribute key="tlcResourcesProfile" value="local custom"/> | ||
| <stringAttribute key="view" value=""/> | ||
| <booleanAttribute key="visualizeStateGraph" value="false"/> | ||
| </launchConfiguration> |