Skip to content

Add model for interaction between Lucene & Version Map on replicas #28

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.

Sign up for GitHub

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

Closed
wants to merge 24 commits into from
Closed

Add model for interaction between Lucene & Version Map on replicas #28

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
a2be1e2
First attempt at a version-map spec
DaveCTurner Feb 13, 2018
aebb6f5
Remove primary and replace with simple request generator. Record max …
DaveCTurner Feb 14, 2018
42b6663
Strengthen invariant
DaveCTurner Feb 14, 2018
b88dba6
Separate out deletion_seqno and indexing_seqno
DaveCTurner Feb 14, 2018
b5efd25
First attempt at optimising append-only indexing
DaveCTurner Feb 15, 2018
d885ff3
Check the deletion map too on unsafe append-only requests
DaveCTurner Feb 15, 2018
0165d83
Remove versions
DaveCTurner Feb 16, 2018
8e8fcfd
Refactoring: advance local check point separately
DaveCTurner Feb 16, 2018
1c00264
Rename INDEX to UPDATE and add ADD request type
DaveCTurner Feb 16, 2018
a90e8f7
Simplify generator
DaveCTurner Feb 16, 2018
cd24b02
Be explicit about the fields in Lucene's operation
DaveCTurner Feb 16, 2018
1cc8354
Use type=ADD rather than a separate append_only flag
DaveCTurner Feb 16, 2018
02ec6cb
Avoid untaken else branches using asserts
DaveCTurner Mar 4, 2018
18fff8e
Improve generator.
DaveCTurner Mar 4, 2018
8b8a3db
Trailing ws
DaveCTurner Mar 4, 2018
0eb43c4
Use state collapsing to model reading duplicate messages
DaveCTurner Mar 6, 2018
2393f2c
Fewer labels needed
DaveCTurner Mar 6, 2018
27c2639
Rename to replica-version-map
DaveCTurner Mar 7, 2018
e0165f1
Extracted out LCP tracker and version-map cleaner as separate async p…
DaveCTurner Mar 8, 2018
4a9343b
Fix comment
DaveCTurner Mar 8, 2018
08e10e8
Remove await hack - move to conditional
DaveCTurner Mar 13, 2018
aa0a43e
Expand comment about refreshes
DaveCTurner Mar 20, 2018
7204b0b
Duplication of ADD operations is not possible
DaveCTurner Mar 20, 2018
9344eb1
Add TODOs
DaveCTurner Mar 20, 2018
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
4 changes: 4 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,10 @@
**/tla/*.toolbox/*.log
**/tla/*.toolbox/*.pdf
**/tla/*.toolbox/*.tex
**/tla/*.toolbox/**/*.tla
**/tla/*.toolbox/**/*.out
**/tla/*.toolbox/**/MC.cfg
**/tla/*.pdf
**/tla/*.old
**/*~
cluster/isabelle/output
432 changes: 432 additions & 0 deletions replica-version-map/tla/versionmap.tla
View file
Open in desktop

Large diffs are not rendered by default.

29 changes: 29 additions & 0 deletions replica-version-map/tla/versionmap.toolbox/.project
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>versionmap</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>toolbox.builder.TLAParserBuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>toolbox.builder.PCalAlgorithmSearchingBuilder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>toolbox.natures.TLANature</nature>
</natures>
<linkedResources>
<link>
<name>versionmap.tla</name>
<type>1</type>
<locationURI>PARENT-1-PROJECT_LOC/versionmap.tla</locationURI>
</link>
</linkedResources>
</projectDescription>
2 changes: 2 additions & 0 deletions replica-version-map/tla/versionmap.toolbox/.settings/org.lamport.tla.toolbox.prefs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
ProjectRootFile=PARENT-1-PROJECT_LOC/versionmap.tla
eclipse.preferences.version=1
Binary file added replica-version-map/tla/versionmap.toolbox/versionmap.tla.pmap
View file
Open in desktop
Binary file not shown.
56 changes: 56 additions & 0 deletions replica-version-map/tla/versionmap.toolbox/versionmap___versionmap.launch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="configurationName" value="versionmap"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="10.136.0.129"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="1"/>
<intAttribute key="maxHeapSize" value="25"/>
<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="local_check_point, request_count, seqnos_above_local_check_point, lucene, pc, isGeneratingRequests, replication_requests, next_seqno, append_only_unsafe_up_to, deletion_seqno, indexing_seqno, replication_request, document"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1NoClientRequestsAtTermination"/>
<listEntry value="1NoReplicationRequestsAtTermination"/>
<listEntry value="1EmptyBuffersAtTermination"/>
<listEntry value="1EqualStatesAtTermination"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="0Termination"/>
</listAttribute>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="NULL;;NULL;1;0"/>
<listEntry value="DELETE;;DELETE;1;0"/>
<listEntry value="CLOSED;;CLOSED;1;0"/>
<listEntry value="OPEN;;OPEN;1;0"/>
<listEntry value="UPDATE;;UPDATE;1;0"/>
<listEntry value="ADD;;ADD;1;0"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value=""/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<stringAttribute key="modelPropertiesExpand" value=""/>
<intAttribute key="numberOfWorkers" value="4"/>
<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="versionmap"/>
<stringAttribute key="view" value=""/>
</launchConfiguration>