Skip to content
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

Jump to bottom

File access rights #1

Open
wants to merge 10 commits into
base: master
Choose a base branch
from
Open

File access rights #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
6c8ff39
add crdt access rights
michael-kamel Jan 25, 2021
be311c8
Midifying MultiValueRegister to provide qeury for AccessRight upper b…
kevinrezae Jan 26, 2021
4951215
first steps towards random datatype value generation
peterzeller Jan 26, 2021
eaeb060
fix typecheck issue
peterzeller Jan 26, 2021
80f9d41
adjust crdt def
michael-kamel Jan 27, 2021
cd657cd
add file access rights crdt
michael-kamel Jan 28, 2021
b6131c0
add file access rights crdt w admin rights
michael-kamel Jan 28, 2021
8c55a2b
add test
michael-kamel Jan 30, 2021
5bc568c
add more tests
michael-kamel Feb 1, 2021
d5efd92
implement upper bound
michael-kamel Feb 2, 2021
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 @@ -10,3 +10,7 @@ act/
jvm/src/main/resources/native
jvm/src/main/resources/scalajs
jvm/src/main/resources/versioninfo.properties
.vscode/
.metals/
project/
.bloop/
3 changes: 3 additions & 0 deletions jvm/src/main/scala/crdtver/language/InputAst.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -276,6 +276,7 @@ object InputAst {
function match {
case BF_isVisible() => s"${args.head} is visible"
case BF_happensBefore(_) => s"(${args.head} happens before ${args(1)})"
case BF_upperBoundedBy() => s"(${args.head} upper bounded by ${args(1)})"
case BF_sameTransaction() => s"sameTransaction(${args(0)}, ${args(1)})"
case BF_less() => s"(${args.head} < ${args(1)})"
case BF_lessEq() => s"(${args.head} <= ${args(1)})"
Expand Down Expand Up @@ -341,6 +342,8 @@ object InputAst {

case class BF_happensBefore(on: HappensBeforeOn) extends BuiltInFunc()

case class BF_upperBoundedBy() extends BuiltInFunc()

sealed trait HappensBeforeOn

object HappensBeforeOn {
Expand Down
20 changes: 20 additions & 0 deletions jvm/src/main/scala/crdtver/language/TypedAstHelper.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,15 @@ object TypedAstHelper {
)
}

def upperBoundedBy(exp1: InExpr, exp2: InExpr): ApplyBuiltin = {
ApplyBuiltin(
source = NoSource(),
typ = BoolType(),
function = BF_upperBoundedBy(),
args = List(exp1, exp2)
)
}

def and(exp1: InExpr, exp2: InExpr): InExpr = (exp1, exp2) match {
case (BoolConst(_, _, true), x) => x
case (x@BoolConst(_, _, false), _) => x
Expand Down Expand Up @@ -286,6 +295,17 @@ object TypedAstHelper {
)
}

/** datatype constructor of type T (type of elements in the register) */
def mkDatatypeCase(name: String, dtype: TypedAst.InTypeExpr, args: TypedAst.InExpr*): TypedAst.FunctionCall =
TypedAst.FunctionCall(
source = NoSource(),
typ = dtype,
functionName = Identifier(NoSource(), name),
typeArgs = List(),
args = args.toList,
kind = FunctionKind.FunctionKindDatatypeConstructor()
)

// def makeOperation(name: String, operationType: InTypeExpr, tArgs: List[InTypeExpr], exp: TypedAst.InExpr*): TypedAst.FunctionCall =
// makeOperationL(name, operationType, tArgs, exp.toList)

Expand Down
2 changes: 2 additions & 0 deletions jvm/src/main/scala/crdtver/language/TypedAstPrinter.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,8 @@ object TypedAstPrinter {
function match {
case BuiltInFunc.BF_isVisible() =>
printExpr(args(0)) <> ".isVisible"
case BuiltInFunc.BF_upperBoundedBy() =>
printOp(args(0), "upperBound", args(1))
case BuiltInFunc.BF_happensBefore(on) =>
printOp(args(0), "happensBefore", args(1))
case BuiltInFunc.BF_sameTransaction() =>
Expand Down
1 change: 1 addition & 0 deletions jvm/src/main/scala/crdtver/language/Typer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -964,6 +964,7 @@ class Typer {
val t = TypeVarUse("T")()
bf match {
case BF_isVisible() => p(List(CallIdType()) -> BoolType())
case BF_upperBoundedBy() => PrincipleType(List(t), List(t, t) -> BoolType()) // TODOO: check
case BF_happensBefore(_) => List(
p(List(CallIdType(), CallIdType()) -> BoolType()),
p(List(InvocationIdType(), InvocationIdType()) -> BoolType())
Expand Down
233 changes: 233 additions & 0 deletions jvm/src/main/scala/crdtver/language/crdts/AFileAccessRightsCrdt.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,233 @@
package crdtver.language.crdts

import crdtver.language.InputAst.{Identifier, NoSource}
import crdtver.language.{TypedAst, crdts}
import crdtver.language.TypedAst.{FunctionKind, InExpr, TypeVarUse}
import crdtver.language.TypedAstHelper._
import crdtver.language.crdts.ACrdtInstance.{QueryStructure, printTypes}


class AFileAccessRightsCrdt extends CrdtTypeDefinition {

/** number of normal type parameters */
override def numberTypes: Int = 1

/** number of CRDT type parameters */
override def numberInstances: Int = 0

private val AFileAccessRightsQry = "AFileAccessRightsQry"

private val RegisterOp = "RegisterOp"

private val Assign = "Assign"

private val ReadPermsUB = "ReadPermsUB"

private val ReadPermsLB = "ReadPermsLB"


override def additionalDataTypes: List[TypedAst.InTypeDecl] = List(
dataType(
RegisterOp,
List("T"),
List(
dtCase(Assign, List("value" -> TypeVarUse("T")())),
)
),
dataType(AFileAccessRightsQry, List("T"),List(
dtCase(ReadPermsUB, List()),
dtCase(ReadPermsLB, List())
)))

override def instantiate(typeArgs: List[TypedAst.InTypeExpr], crdtArgs: List[ACrdtInstance]): ACrdtInstance = new ACrdtInstance {

override def toString: String = s"${AFileAccessRightsCrdt.this.name}${printTypes(typeArgs, crdtArgs)}"

val T: TypedAst.InTypeExpr = typeArgs.head

override def operationType: TypedAst.InTypeExpr = TypedAst.SimpleType(RegisterOp, List(T))()

override def queryType: TypedAst.InTypeExpr = TypedAst.SimpleType(AFileAccessRightsQry, List(T))()

override def queryReturnType(q: QueryStructure): TypedAst.InTypeExpr = q match {
case QueryStructure(ReadPermsUB, List()) => T
case QueryStructure(ReadPermsLB, List()) => T
}

override def queryDefinitions(): List[TypedAst.InQueryDecl] = List(
queryDeclEnsures(ReadPermsUB, List(), T, {
val result = varUse("result", T)
val result2 = varUse("result2", T)
val upperBound = varUse("result", T)
val someValue = varUse("someValue", T)
val someValue2 = varUse("someValue2", T)
val someAssign = varUse("someAssign", T)
val someAssign2 = varUse("someAssign", T)


val relevantCall = varUse("relevantCall")
val relevantCall2 = varUse("relevantCall2")
val otherCall = varUse("otherCall")
val otherCall2 = varUse("otherCall2")


forall(relevantCall, forall(someAssign,
( relevantCall.isVis
&& relevantCall.op === makeOp(Assign, someAssign)
&& not(exists(otherCall, exists(someValue, otherCall.isVis && relevantCall < otherCall && otherCall.op === makeOp(Assign, someValue))))
// all uninterrupted Assigns to the register
) -->
(
(_upperBoundedByOrEq(someAssign, result))// upper bound
)
)) &&
(
forall(result2,
(
forall(relevantCall2, forall(someAssign2,
(
relevantCall2.isVis
&& relevantCall2.op === makeOp(Assign, someAssign2)
&& not(exists(otherCall2, exists(someValue2, otherCall2.isVis && relevantCall2 < otherCall2 && otherCall2.op === makeOp(Assign, someValue2))))
) -->
(
_upperBoundedByOrEq(someAssign2, result2)
)
))
) -->
(
_upperBoundedByOrEq(result, result2)
))
)
}),
queryDeclEnsures(ReadPermsLB, List(), T, {
val result = varUse("result", T)
val result2 = varUse("result2", T)
val upperBound = varUse("result", T)
val someValue = varUse("someValue", T)
val someValue2 = varUse("someValue2", T)
val someAssign = varUse("someAssign", T)
val someAssign2 = varUse("someAssign", T)


val relevantCall = varUse("relevantCall")
val relevantCall2 = varUse("relevantCall2")
val otherCall = varUse("otherCall")
val otherCall2 = varUse("otherCall2")

forall(relevantCall, forall(someAssign,
( relevantCall.isVis
&& relevantCall.op === makeOp(Assign, someAssign)
&& not(exists(otherCall, exists(someValue, otherCall.isVis && relevantCall < otherCall && otherCall.op === makeOp(Assign, someValue))))
// all uninterrupted Assigns to the register
) -->
(
(_lowerBoundedByOrEq(someAssign, result))// upper bound
)
)) &&
(
forall(result2,
(
forall(relevantCall2, forall(someAssign2,
(
relevantCall2.isVis
&& relevantCall2.op === makeOp(Assign, someAssign2)
&& not(exists(otherCall2, exists(someValue2, otherCall2.isVis && relevantCall2 < otherCall2 && otherCall2.op === makeOp(Assign, someValue2))))
) -->
(
_lowerBoundedByOrEq(someAssign2, result2)
)
))
) -->
(
_lowerBoundedByOrEq(result, result2)
))
)
})
)

override def additionalDataTypesRec: List[TypedAst.InTypeDecl] = AFileAccessRightsCrdt.this.additionalDataTypes

def _upperBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = (
(
val1 === mkDatatypeCase("ANone", T) &&
(val2 === mkDatatypeCase("ANone", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) || val2 === mkDatatypeCase("ARW", T))
) ||
(
val1 === mkDatatypeCase("AR", T) &&
(val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("ARW", T))
) ||
(
val1 === mkDatatypeCase("AW", T) &&
(val2 === mkDatatypeCase("AW", T) || val2 === mkDatatypeCase("ARW", T))
) ||
(
val1 === mkDatatypeCase("ARW", T) &&
val2 === mkDatatypeCase("ARW", T)
) ||
(
val1 === mkDatatypeCase("UNone", T) &&
( val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("UR", T) || val2 === mkDatatypeCase("UW", T) || val2 === mkDatatypeCase("UNone", T)
|| val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T))
) ||
(
val1 === mkDatatypeCase("UR", T) &&
( val2 === mkDatatypeCase("UR", T) || val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("ARW", T)
|| val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T))
) ||
(
val1 === mkDatatypeCase("UW", T) &&
( val2 === mkDatatypeCase("UW", T) || val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("ARW", T)
|| val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T))
) ||
(
val1 === mkDatatypeCase("URW", T) &&
( val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("ARW", T)
|| val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T))
)
)

def _lowerBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = (
(
val1 === mkDatatypeCase("ANone", T) &&
val2 === mkDatatypeCase("ANone", T)
) ||
(
val1 === mkDatatypeCase("AR", T) &&
(val2 === mkDatatypeCase("ANone", T) || val2 === mkDatatypeCase("AR", T))
) ||
(
val1 === mkDatatypeCase("AW", T) &&
(val2 === mkDatatypeCase("ANone", T) || val2 === mkDatatypeCase("AW", T))
) ||
(
val1 === mkDatatypeCase("ARW", T) &&
(val2 === mkDatatypeCase("ANone", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) || val2 === mkDatatypeCase("ARW", T))
) ||
(
val1 === mkDatatypeCase("UNone", T) &&
(val2 === mkDatatypeCase("UNone", T) || val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T)
||val2 === mkDatatypeCase("ANone", T))
) ||
(
val1 === mkDatatypeCase("UR", T) &&
(val2 === mkDatatypeCase("UR", T) || val2 === mkDatatypeCase("UNone", T) || val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T)
|| val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T))
) ||
(
val1 === mkDatatypeCase("UW", T) &&
(val2 === mkDatatypeCase("UW", T) || val2 === mkDatatypeCase("UNone", T) || val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T)
|| val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T))
) ||
(
val1 === mkDatatypeCase("URW", T) &&
( val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("UR", T) || val2 === mkDatatypeCase("UW", T) || val2 === mkDatatypeCase("UNone", T)
|| val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T))
)
)
}

/** name of the CRDT */
override def name: String = "AFileAccessRights"
}

2 changes: 2 additions & 0 deletions jvm/src/main/scala/crdtver/language/crdts/CrdtTypeDefinition.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,8 @@ object CrdtTypeDefinition {
new MapCrdt(DW(), MapCrdt.DeleteAffectsPriorAndConcurrent(), "Map_dw"),
new RegisterCrdt,
new MVRegisterCrdt,
new FileAccessRightsCrdt,
new AFileAccessRightsCrdt,
new CounterCrdt
)

Expand Down
Loading