diff --git a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/ProjectNotes/index.xml b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/ProjectNotes/index.xml index 03f741c..4b02c93 100644 --- a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/ProjectNotes/index.xml +++ b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/ProjectNotes/index.xml @@ -1,6 +1,6 @@ - + - + General \ No newline at end of file diff --git a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/binder.backup b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/binder.backup index 3bb514a..57f6f7f 100644 Binary files a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/binder.backup and b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/binder.backup differ diff --git a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/search.indexes b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/search.indexes index 9f3720e..a75764f 100644 --- a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/search.indexes +++ b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Files/search.indexes @@ -1,4 +1,4 @@ - + @@ -184,11 +184,18 @@ Mitigation strategies 3. Never have your programs ask for more rights than they need, to data, to database tables (and in HBase and Accumulo: columns) 4. Log data in a form which can be used for audit logs. (Issue: what is our story here? Logging to local/remote filesystems isn't it, not if malware could overwrite the logs) - - Discussion - Discussion + + Response to Reviewers' Comments + Response to Reviewers’ Comments -[Insert text here] +We appreciate the detailed comments and suggestions from the reviewers. We have provided our responses below the corresponding comment. + +Reviewer 1 +[Insert reviewers’ comments here] + +[Authors] + +<$fullname> UGI @@ -280,18 +287,8 @@ If you find yourself down at this level you are in trouble. Bear that in mind. Gists - - Response to Reviewers' Comments - Response to Reviewers’ Comments - -We appreciate the detailed comments and suggestions from the reviewers. We have provided our responses below the corresponding comment. - -Reviewer 1 -[Insert reviewers’ comments here] - -[Authors] - -<$fullname> + + Figures Kerberos setup commands @@ -618,8 +615,11 @@ This means that the caller did not have the credentials to talk to a Kerberos-se Past copies Duplicate important drafts into here. - - Figures + + Discussion + Discussion + +[Insert text here] ZOOKEEPER and SASL diff --git a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/QuickLook/Thumbnail.jpg b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/QuickLook/Thumbnail.jpg index fd38b6c..9902d53 100644 Binary files a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/QuickLook/Thumbnail.jpg and b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/QuickLook/Thumbnail.jpg differ diff --git a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Settings/ui.plist b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Settings/ui.plist index 4278521..c3f1d4b 100644 --- a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Settings/ui.plist +++ b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/Settings/ui.plist @@ -46,8 +46,8 @@ 0 binderSplitFrames - {{0, 0}, {205, 981}} - {{206, 0}, {1489, 981}} + {{0, 0}, {174, 756}} + {{175, 0}, {1265, 756}} binderState @@ -140,7 +140,7 @@ mainDocumentEditor.lockedInPlace mainDocumentEditor.scrollRect - {{0, 0}, {606, 304}} + {{0, 0}, {621, 304}} mainDocumentEditor.selectedItemIDs mainDocumentEditor.textEditorState @@ -1002,15 +1002,60 @@ title label status + createdDate + modifiedDate + words + characters + includeInExport + pageBreakBefore + compileAsIs + targetCount + targetCountType + progress + totalWords + totalCharacters + allKeywords + totalTargetCount + totalProgress widths + allKeywords + 64 + characters + 46 + compileAsIs + 110.841796875 + createdDate + 53 + includeInExport + 20 label 114.296875 + modifiedDate + 50 + pageBreakBefore + 66 + progress + 50.041019439697266 status 93.92578125 + targetCount + 50 + targetCountType + 50 title 246 + totalCharacters + 96 + totalProgress + 64 + totalTargetCount + 64 + totalWords + 72 + words + 40 supportingDocumentEditor.outlinerState @@ -1019,7 +1064,7 @@ 10 supportingDocumentEditor.scrollRect - {{0, 0}, {1179.2, 702.40002}} + {{0, 0}, {1012, 522.40002}} supportingDocumentEditor.selectedRanges {13, 0} supportingDocumentEditor.textEditorState diff --git a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/kerberos_the_madness.scrivx b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/kerberos_the_madness.scrivx index b26220c..903ab0d 100644 --- a/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/kerberos_the_madness.scrivx +++ b/the_madness_beyond_the_gate/book/kerberos_the_madness.scriv/kerberos_the_madness.scrivx @@ -1,7 +1,7 @@ - - + + - + Draft Yes @@ -14,7 +14,7 @@ - + Front page Yes @@ -26,7 +26,7 @@ 16,0 - + Main content Yes @@ -37,7 +37,7 @@ 0,0 - + Introduction 5 @@ -48,7 +48,7 @@ 206,0 - + Foundational Concepts 5 @@ -59,7 +59,7 @@ 4,0 - + The Limits of Hadoop Security 5 @@ -70,7 +70,7 @@ 3203,0 - + Hadoop IPC Security 5 @@ -81,7 +81,7 @@ 646,0 - + UGI Yes @@ -91,7 +91,7 @@ 2,0 - + SPNEGO 5 @@ -102,7 +102,7 @@ 1239,0 - + ZOOKEEPER and SASL 5 @@ -113,7 +113,7 @@ 833,0 - + java.security.krb5.conf 5 @@ -124,7 +124,7 @@ 1143,0 - + JAAS Configuration 5 @@ -135,7 +135,7 @@ 2,0 - + Logging Yes @@ -145,7 +145,7 @@ 13,0 - + Error Messages to Fear Yes @@ -155,7 +155,7 @@ 2437,0 - + Kerberos Tests with MiniKDC Yes @@ -165,7 +165,7 @@ 2,0 - + Testing against Kerberized Hadoop clusters Yes @@ -175,7 +175,7 @@ 140,0 - + Low-level secrets Yes @@ -185,7 +185,7 @@ 2,0 - + Checklists Yes @@ -197,7 +197,7 @@ - + Acknowledgements Yes @@ -208,7 +208,7 @@ 510,0 - + References Yes @@ -219,7 +219,7 @@ 205,36 - + Figure legends Yes @@ -229,7 +229,7 @@ 0,72 - + Tables Yes @@ -240,7 +240,7 @@ 0,0 - + Table 1 Yes @@ -253,7 +253,7 @@ - + Figures Yes @@ -265,7 +265,7 @@ 0,0 - + Configuring Firefox for SPNEGO Yes @@ -280,7 +280,7 @@ - + Templates Yes @@ -290,7 +290,7 @@ 0,0 - + Table X Yes @@ -302,7 +302,7 @@ 47,0 - + Cover letter Yes @@ -313,7 +313,7 @@ 414,0 - + Response to Reviewers' Comments Yes @@ -324,7 +324,7 @@ 94,0 - + Gists Yes @@ -334,7 +334,7 @@ 0,0 - + META-INF/services/org.apache.hadoop.security.SecurityInfo Yes @@ -346,7 +346,7 @@ - + Chapter Yes @@ -358,13 +358,13 @@ - + Research Yes - + Abstract & keywords Yes @@ -375,7 +375,7 @@ 111,0 - + Kerberos setup commands Yes @@ -385,7 +385,7 @@ 5814,83 - + Hadoop and Kerberos Yes @@ -397,7 +397,7 @@ - + Ideas 0,0 @@ -407,7 +407,7 @@ 0,0 - + To-Do List 0,0 @@ -417,13 +417,13 @@ 39,0 - + Trash Yes - + Methods Yes @@ -433,7 +433,7 @@ 0,0 - + Patients Yes @@ -444,7 +444,7 @@ 35,0 - + Methods/interventions Yes @@ -455,7 +455,7 @@ 8,18 - + Outcome measurements Yes @@ -466,7 +466,7 @@ 21,18 - + Statistical analysis Yes @@ -479,7 +479,7 @@ - + Past copies 0,0 @@ -488,7 +488,7 @@ 0,0 - + 20062014 Submitted to [journal] 1 @@ -501,7 +501,7 @@ - + # Licensed to the Apache Software Foundation (ASF) under Yes @@ -511,7 +511,7 @@ 0,0 - + Methods Yes @@ -522,7 +522,7 @@ 0,27 - + Results Yes @@ -533,7 +533,7 @@ 7,0 - + Discussion Yes @@ -544,7 +544,7 @@ 10,0 - + Background and Significance Yes @@ -555,7 +555,7 @@ 47,0 - + Conclusion Yes @@ -565,7 +565,7 @@ 10,0 - + Untitled Yes @@ -575,7 +575,7 @@ 0,0 - + Untitled Yes @@ -585,7 +585,7 @@ 0,0 - + Untitled Yes @@ -595,7 +595,7 @@ 0,0 - + Notes of Obscurity Yes @@ -605,7 +605,7 @@ 20,0 - + References-1 Yes @@ -657,9 +657,9 @@ Loughran - 0 + 0 0 - + 22 diff --git a/tlaspecs/blobstore/objectstore.tla b/tlaspecs/blobstore/objectstore.tla index 7614304..54c651a 100644 --- a/tlaspecs/blobstore/objectstore.tla +++ b/tlaspecs/blobstore/objectstore.tla @@ -39,56 +39,69 @@ The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL This specification defines -1. A model of an object store: a consistent store of data and metadata, - one without any notion of a "directory hierarchy". It is intended to model - object stores such as Amazon S3 and OpenStack swift, while leaving scope for - optional features which may only be available on other stores. +* A model of a consistent object store: a consistent store of data and metadata, + one without any notion of a "directory hierarchy". It is intended to model + object stores such as Amazon S3, and includes its multipart PUT API. -2. An API for communicating with object stores from Hadoop filesystems. - -3. How the Object Store API must translate into changes in the state of the Object Store - itself. That is: what MUST an implementation do? +* An API for communicating with object stores from Hadoop filesystems. +It is intended to be a foundation for defining algorithms with worth +with S3, such as the s3guard commit algorithm. ============================================================================ *) CONSTANTS - Paths, \* the non-finite set of all possible valid paths - Data, \* the non-finite set of all possible sequences of bytes - MetadataKeys, \* the set of all possible metadata keys + Paths, \* the non-finite set of all possible valid paths + PathsAndRoot, \* Paths and the "root" path; the latter is read-only + Data, \* the non-finite set of all possible sequences of bytes + MetadataKeys, \* the set of all possible metadata keys MetadataValues, \* the non-finite set of all possible metadata values - Timestamp, \* A timestamp - Byte - + Timestamp, \* A timestamp + Byte, + Etag, + MultipartPutId, + PartId, + NonEmptyString -ASSUME Paths \in (STRING \ "") +ASSUME NonEmptyString \in (STRING \ "") +ASSUME PathsAndRoot \in STRING +ASSUME Paths \in (PathsAndRoot \ "") -(* There are some metadata keys which are system MD entries. Those MAY be queried but SHALL NOT be explictly set. *) +(* There are some metadata keys which are system metadata entries. + Those MAY be queried but SHALL NOT be explictly set. (more specifically, they'll be ignored if you try. *) -ASSUME MetadataKeys \in (STRING \ "") +ASSUME MetadataKeys \in NonEmptyString -ASSUME MetadataValues \in (STRING \ "") +ASSUME MetadataValues \in STRING \* Timestamps are positive integers since the epoch. ASSUME Timestamp \in Nat /\ Timestamp > 0 -ASSUME Byte \in 0..256 +\* Byte type +ASSUME Byte \in 0..255 + +(* Data is a sequence of bytes *) +ASSUME Data \in Seq(Byte) + +ASSUME Etag \in NonEmptyString +ASSUME MultipartPutId \in NonEmptyString -ASSUME Data \in Seq(Byte) +(* Only 11,000 parts are allowed *) +ASSUME PartId \in 1..11000 ---------------------------------------------------------------------------------------- -(* +(* There is a predicate to validate a pathname. This is considered implementation-specific. It could be describable as a regular expression specific to each implementation, - though constraints such as "no two adjacent '/' characters" might make for a complex regexp. + though constraints such as "no two adjacent '/' characters" might make for a complex regexp. Perhaps each FS would have a set of regexps which all must be valid for a path to be considered valid. *) @@ -108,17 +121,33 @@ ASSUME \A e \in MetadataKeys: is_valid_metadata_key(e) \in BOOLEAN CONSTANT path_matches(_, _, _) -(* This should really be defined by looking inside the strings. + +(* This should really be defined by looking inside the strings. It is: all paths starting with the prefix up to those ending in the suffix *) ASSUME \A p \in Paths, prefix, delimiter \in Paths: path_matches(p, prefix, delimiter) \in BOOLEAN +(* A function to return an etag of some data *) +CONSTANT etag_of(_) + +(* A function to return an etag of a multipart operation; implementation specific*) +CONSTANT etag_of_multipart_operation(_) + +(* Etags are strings, hence in MetadataValues. *) +ASSUME \A d \in Data: etag_of(d) \in Etag + +(* +This is commented out as it is not a requirement that etags are the same for an equivalent sequence +of bytes. All that matters is that one is generated. +ASSUME \A d, e \in Data: d = e => etag_of(d) = etag_of(e) \in STRING +*) + ---------------------------------------------------------------------------------------- -VARIABLES - store \* The object store - +VARIABLE store \* The object store +VARIABLE pending \* Pending requests + ---------------------------------------------------------------------------------------- @@ -133,41 +162,67 @@ Success == "Success" MetadataEntry == [ - key: MetadataKeys, \* The key of the entry - value: MetadataValues \* the value of this metadata entry - ] + key: MetadataKeys, \* The key of the entry + value: MetadataValues \* the value of this metadata entry +] SystemMetadata == [ size: Nat, created: Timestamp - ] +] (* A store : path -> (data, user-md, system-md) update: PUT, DELETE -query: GET, HEAD, LIST(path) -*) +query: GET, HEAD, LIST(path) +*) StoreEntry == [ - data: Data , \* the data in the entry - created: Timestamp \* timestamp + data: Data , \* the data in the entry + created: Timestamp, \* timestamp + etag: MetadataValues ] ListingEntry == [ path: Paths, \* The path to the entry data: Data , \* the data in the entry - created: Timestamp, \* timestamp + created: Timestamp, \* timestamp + etag: MetadataValues, metadata: MetadataEntry \* it's a set ] - + (* The check for a path having an entry is pulled out for declaring invariants *) has_entry(s, p) == p \in DOMAIN s +PendingMultipartPartRequest == [ + putId: MultipartPutId, + part: PartId, + data: Data +] + +PendingMultipartPartResponse == [ + etag: Etag +] + +PendingMultipartPutPart == [ + data: Data, + etag: Etag +] + + +(* A pending Multipart Upload has an ID and start timne, which is used to define the final + create time of the committed operation *) +PendingMultipartOperation == [ +\* id: STRING, + path: Paths, + started: Timestamp, + parts: [PartId -> PendingMultipartPutPart] +] (* @@ -179,19 +234,19 @@ for those implementors planning to write tests. StoreStateInvariant == /\ store \in [Paths -> StoreEntry] - /\ \A path \in DOMAIN store: has_entry(store, path) - /\ \A path \in (Paths \ DOMAIN store): ~has_entry(store, path) - - + /\ pending \in [MultipartPutId -> PendingMultipartOperation] + + (* The initial state of the store is that it is empty. *) (* Notice how this ignores the root entry, "". This is a special entry: object stores are not filesystems: there is no root node equivalent to "/" *) InitialStoreState == /\ StoreStateInvariant /\ DOMAIN store = {} + /\ DOMAIN pending = {} ----- +---- (* Actions. @@ -207,48 +262,46 @@ final state for testability doPut(path, data, current_time, result) == LET validArgs == path \in Paths /\ data \in Data /\ current_time \in Timestamp - IN + IN \/ /\ ~validArgs /\ result' = BadRequest - /\ UNCHANGED store + /\ UNCHANGED <> \/ /\ validArgs /\ result' = Success - /\ store' = [store EXCEPT ![path] = [data |-> data, created |-> current_time]] + /\ UNCHANGED pending + /\ store' = [store EXCEPT ![path] = [data |-> data, created |-> current_time, etag |-> etag_of(data)]] (* GET: path -> data as well as summary metadata -*) +*) doGet(path, result, metadata, data) == LET - validArgs == path \in Paths /\ data \in Data + validArgs == path \in PathsAndRoot exists == has_entry(store, path) - IN + entry == store[path] + IN \/ /\ ~validArgs /\ result' = BadRequest - /\ UNCHANGED store + /\ UNCHANGED <> + + \/ /\ validArgs + /\ path = "" + /\ result' = Success + /\ UNCHANGED <> + /\ data' = {} + \/ /\ validArgs /\ ~exists /\ result' = NotFound - /\ UNCHANGED store + /\ UNCHANGED <> + \/ /\ validArgs /\ exists /\ result' = Success /\ data' = store[path].data - /\ metadata' = [created |-> store[path].created, length |-> Len(store[path].data)] - /\ UNCHANGED store - -(* -HEAD: the metadata without the data -*) - -(* -doHead2(path, result, metadata) == - LET - data == d \in Data - IN - doGet(path, result', data, metadata') -*) + /\ metadata' = [created |-> entry.created, length |-> Len(entry.data), etag |-> entry.etag] + /\ UNCHANGED <> (* HEAD: the metadata without the data @@ -256,57 +309,72 @@ HEAD: the metadata without the data doHead(path, result, metadata) == LET - validArgs == path \in Paths + validArgs == path \in PathsAndRoot exists == has_entry(store, path) - IN + entry == store[path] + IN \/ /\ ~validArgs /\ result' = BadRequest - /\ UNCHANGED store + /\ UNCHANGED <> + + \/ /\ validArgs + /\ path = "" + /\ result' = Success + /\ metadata' = [created |-> 0, length |-> 0] + /\ UNCHANGED <> + \/ /\ validArgs /\ ~exists /\ result' = NotFound - /\ UNCHANGED store + /\ UNCHANGED <> + \/ /\ validArgs /\ exists /\ result' = Success - /\ metadata' = [created |-> store[path].created, length |-> Len(store[path].data)] - /\ UNCHANGED store + /\ metadata' = [created |-> entry.created, length |-> Len(entry.data), etag |-> entry.etag] + /\ UNCHANGED <> doDelete(path, result) == LET validArgs == path \in Paths exists == has_entry(store, path) - IN + IN \/ /\ ~validArgs /\ result' = BadRequest - /\ UNCHANGED store + /\ UNCHANGED <> + \/ /\ validArgs /\ ~exists /\ result' = NotFound - /\ UNCHANGED store + /\ UNCHANGED <> + \/ /\ validArgs /\ exists /\ result' = Success /\ store' = [p \in (DOMAIN store \ path) |-> store[p]] + /\ UNCHANGED pending doCopy(source, dest, current_time, result) == LET - validArgs == source \in Paths /\ dest \in Paths /\ current_time \in Timestamp - exists == has_entry(store, source) - IN + validArgs == source \in Paths /\ dest \in Paths /\ current_time \in Timestamp + exists == has_entry(store, source) + IN \/ /\ ~validArgs /\ result' = BadRequest - /\ UNCHANGED store + /\ UNCHANGED <> + \/ /\ validArgs /\ ~exists /\ result' = NotFound - /\ UNCHANGED store + /\ UNCHANGED <> + \/ /\ validArgs /\ exists /\ result' = Success /\ store' = [store EXCEPT ![dest] = [data |-> store[source].data, created |-> current_time]] + /\ UNCHANGED pending (* The list operation returns the metadata of all entries in the object store whose path matches the prefix/suffix pattern. S3 also returns a string sequence of common subpath underneath, essential "what look like directories" *) @@ -314,19 +382,113 @@ S3 also returns a string sequence of common subpath underneath, essential "what pathsMatchingPrefix(prefix, suffix) == \A path \in DOMAIN store : path_matches(path, prefix, suffix) doList(prefix, suffix, result, listing) == - /\ prefix \in STRING - /\ suffix \in STRING - /\ result' = Success - /\ listing' = [path \in pathsMatchingPrefix(prefix, suffix) |-> - [path |-> path, created |-> store[path].created, length |-> Len(store[path].data)]] - /\ UNCHANGED store + LET + validArgs == prefix \in STRING /\ suffix \in STRING + IN + \/ /\ ~validArgs + /\ result' = BadRequest + /\ UNCHANGED <> + + \/ /\ validArgs + /\ result' = Success + /\ listing' = [path \in pathsMatchingPrefix(prefix, suffix) |-> + [path |-> path, created |-> store[path].created, length |-> Len(store[path].data), etag |-> store[path].etag]] + /\ UNCHANGED <> +(* +Initiate a multipart PUT. The destination is specified; the create time of the final artifact is set to the current server time. +A unique ID is returned. +There is no requirement for the destination to be unique: multiple requests may target the same destination, with the order of the commit +operation defining the order in which the results become visible. +*) + + +doInitiateMultipartPut(dest, current_time, result, operationId) == + LET + validArgs == dest \in Paths /\ current_time \in Timestamp + newPartId == CHOOSE id \in MultipartPutId: ~id \in DOMAIN pending + IN + \/ /\ ~validArgs + /\ result' = BadRequest + /\ UNCHANGED <> + + \/ /\ validArgs + /\ result' = Success + /\ UNCHANGED store + /\ operationId' = newPartId + /\ pending' = [pending EXCEPT ![newPartId] = [path |-> dest, created |-> current_time]] + +(* +PUT a single part for an operation +*) +doPutPart(operationId, partId, part_data, result, etagResult) == + LET + validArgs == operationId \in DOMAIN pending /\ part_data \in Data /\ partId \in PartId + etagVal == etag_of(part_data) + IN + \/ /\ ~validArgs + /\ result' = BadRequest + /\ UNCHANGED <> + + \/ /\ validArgs + /\ result' = etagVal + /\ etagResult' = etagVal + /\ UNCHANGED store + /\ pending' = [pending EXCEPT + ![operationId] = [ + path |-> pending[operationId].dest, + parts |-> [pending[operationId].parts EXCEPT ![partId] = [data |-> part_data, etag |-> etagVal] ] + ] + ] + +(* + The commit operation is the most complex. The part list supplied defines the order in which the supplied parts + are saved to the store. + TODO: work out how to declare that all data is the ordered appending of the data of the list of parts. Recurse? +*) +doCommitMultipartPut(operationId, parts, result) == + LET + upload == pending[operationId] + validArgs == (operationId \in DOMAIN pending) /\ (parts \in Seq(PartId)) + /\ (\A p \in parts: p \in DOMAIN upload.parts) /\ (\A p \in DOMAIN upload.parts: p \in parts) + \* alldata == \A [part \in (1...Len(parts) -1]) Append(upload[parts[part]], upload[parts[part + 1]) + alldata == parts + etag == etag_of_multipart_operation(upload) + IN + \/ /\ ~validArgs + /\ result' = BadRequest + /\ UNCHANGED <> + + \/ /\ validArgs + /\ result' = Success + /\ pending' = [p \in (DOMAIN pending \ operationId) |-> pending[p]] + /\ store' = [store EXCEPT ![upload.path] = [data |-> alldata, created |-> upload.created, etag |-> etag]] + + +(* + Abort the multipart put operation. + All pending data is deleted; the pending operation record removed. + *) +doAbortMultipartPut(operationId, result) == +LET + validArgs == operationId \in DOMAIN pending +IN + \/ /\ ~validArgs + /\ result' = BadRequest + /\ UNCHANGED <> + + \/ /\ validArgs + /\ result' = Success + /\ UNCHANGED store + /\ pending' = [p \in (DOMAIN pending \ operationId) |-> pending[p]] + + --------- \* PutInvariant == \A p in Paths: doDelete(p, Success) => ~has_entry(store', p) - + \* DeleteInvariant == \A p in Paths: doDelete(p, Success) => ~has_entry(store', p) @@ -343,16 +505,16 @@ GetLengthInvariant == (* GetAndHeadInvariant == \A path \in DOMAIN store, sysMd \in SystemMetadata, data \in Data : - doGet(path, Success, data, sysMd) ==> doHead(path, Success, sysMd) + doGet(path, Success, data, sysMd) ==> doHead(path, Success, sysMd) *) (* The details you get back in a listing match the details you get back from a doGet call on the specific path *) (* of course, on an eventually consistent object store, there may be lag *) (* - - ListAndGetInvariant == TODO - + + ListAndGetInvariant == TODO + *) @@ -400,7 +562,7 @@ listAction == [ (* Process a request, generate a result. *) (* TODO: merge GET data into result *) (* -process(request, result, current_time) == +process(request, result, current_time) == LET verb == request.verb IN \/ verb = "PUT" /\ doPut(request.path, request.data, current_time, result) @@ -409,7 +571,7 @@ process(request, result, current_time) == \/ verb = "DELETE" /\ doDelete(request.path, result) \/ verb = "COPY" /\ doCopy(request.source, request.dest, current_time, result) \/ verb = "LIST" /\ doList(request.prefix, request.suffix, result) - + *) @@ -422,7 +584,7 @@ THEOREM InitialStoreState => []StoreStateInvariant ============================================================================= \* Modification History -\* Last modified Thu Oct 06 15:30:47 BST 2016 by stevel +\* Last modified Sun Feb 19 22:19:11 GMT 2017 by stevel \* Created Sun Jun 19 18:07:44 BST 2016 by stevel