Skip to content
Snippets Groups Projects
Commit 5748b2e3 authored by Tobias Pietzsch's avatar Tobias Pietzsch
Browse files

WeakRefCache verified get( key, loader, hint ) for all hint variants.

parent 08269ea2
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/main/java/verify/SatPlayground.java
+ 201
− 39
View file @ 5748b2e3
...@@ -313,7 +313,8 @@ public class SatPlayground ...@@ -313,7 +313,8 @@ public class SatPlayground
} }
} }
final String padded = String.format("%1$-" + padlen + "s", name ); final String padded = String.format("%1$-" + padlen + "s", name );
System.out.println( "(" + t + ") " + padded + " : " + possible ); final String time = String.format("%1$" + 5 + "s", String.format( "(%d) ", t ) );
System.out.println( time + padded + " : " + possible );
} }
protected void debugprintPossibleStates() protected void debugprintPossibleStates()
...@@ -493,13 +494,34 @@ public class SatPlayground ...@@ -493,13 +494,34 @@ public class SatPlayground
final Program ifProg, final Program ifProg,
final String elseName, final String elseName,
final Program elseProg ) final Program elseProg )
{
this( condition, ifName, ifProg, null, elseName, elseProg );
}
public Branch(
final BranchCondition condition,
final String ifName,
final Program ifProg,
final BranchCondition elsecondition,
final String elseName,
final Program elseProg )
{ {
super( "(--branch--)" ); super( "(--branch--)" );
this.ref = condition.v; this.ref = condition.v;
final Collection< State > ifStates = condition.states; final Collection< State > ifStates = condition.states;
final ArrayList< State > elseStates = new ArrayList<>( Arrays.asList( State.values() ) ); final ArrayList< State > elseStates = new ArrayList<>();
elseStates.removeAll( ifStates ); if ( elsecondition != null )
{
elseStates.addAll( elsecondition.states );
if ( elsecondition.v != condition.v )
throw new IllegalArgumentException();
}
else
{
elseStates.addAll( Arrays.asList( State.values() ) );
elseStates.removeAll( ifStates );
}
final Program pTrue = new Program( ifName ) final Program pTrue = new Program( ifName )
{ {
...@@ -640,6 +662,25 @@ public class SatPlayground ...@@ -640,6 +662,25 @@ public class SatPlayground
} }
} }
/**
*
*/
static class Unlock extends Program
{
public Unlock( final String name )
{
super( name );
}
@Override
protected void modifyState( final ProblemState state ) throws ContradictionException
{
state.unblock( transition( A, B ) );
state.unblock( transition( A, C ) );
state.unblock( transition( B, C ) );
}
}
/** /**
* *
*/ */
...@@ -748,6 +789,11 @@ public class SatPlayground ...@@ -748,6 +789,11 @@ public class SatPlayground
return new Lock( name ); return new Lock( name );
} }
public static Program unlock( final String name )
{
return new Unlock( name );
}
public static Program remove( final String name ) public static Program remove( final String name )
{ {
return new RemoveEntryFromMap( name ); return new RemoveEntryFromMap( name );
...@@ -758,6 +804,11 @@ public class SatPlayground ...@@ -758,6 +804,11 @@ public class SatPlayground
return new Branch( c, ifseq.name, ifseq.program, elseseq.name, elseseq.program ); return new Branch( c, ifseq.name, ifseq.program, elseseq.name, elseseq.program );
} }
public static Program branch( final BranchCondition ifcond, final IfSeq ifseq, final BranchCondition elsecond, final ElseSeq elseseq )
{
return new Branch( ifcond, ifseq.name, ifseq.program, elsecond, elseseq.name, elseseq.program );
}
public static BranchCondition cond( final ValueRef v, final State ... states ) public static BranchCondition cond( final ValueRef v, final State ... states )
{ {
return new BranchCondition( v, Arrays.asList( states ) ); return new BranchCondition( v, Arrays.asList( states ) );
...@@ -806,6 +857,7 @@ public class SatPlayground ...@@ -806,6 +857,7 @@ public class SatPlayground
final ValueRef v2 = new ValueRef(); final ValueRef v2 = new ValueRef();
final ValueRef v3 = new ValueRef(); final ValueRef v3 = new ValueRef();
final ValueRef v4 = new ValueRef(); final ValueRef v4 = new ValueRef();
final ValueRef v5 = new ValueRef();
System.out.println( "CacheHints == VOLATILE" ); System.out.println( "CacheHints == VOLATILE" );
System.out.println( "======================" ); System.out.println( "======================" );
...@@ -824,7 +876,8 @@ public class SatPlayground ...@@ -824,7 +876,8 @@ public class SatPlayground
nop( " return v;" ) nop( " return v;" )
), ),
elseseq( " } else {", elseseq( " } else {",
branch( cond( B ), branch(
cond( B, D, E, F ),
ifseq( " if ( loaded == INVALID ) {", ifseq( " if ( loaded == INVALID ) {",
getv( " v = entry.getValue();", v3 ), getv( " v = entry.getValue();", v3 ),
branch( cond( v3, B, C ), branch( cond( v3, B, C ),
...@@ -838,6 +891,7 @@ public class SatPlayground ...@@ -838,6 +891,7 @@ public class SatPlayground
) )
) )
), ),
cond( A, C, D, E, F ),
elseseq( " } else { // loaded == VALID", elseseq( " } else { // loaded == VALID",
getv( " v = entry.getValue();", v4 ), getv( " v = entry.getValue();", v4 ),
branch( cond( v4, B, C ), branch( cond( v4, B, C ),
...@@ -854,9 +908,9 @@ public class SatPlayground ...@@ -854,9 +908,9 @@ public class SatPlayground
) )
) )
), ),
elseseq( "} else { // v != null ", elseseq( "} else { // v != null ",
nop( " if ( !v.isValid() ) { enqueue(); } " ), nop( " if ( !v.isValid() ) { enqueue(); } " ),
nop( " return v; // strong ref (1)" ) nop( " return v; // strong ref (1)" )
) )
) )
); );
...@@ -881,21 +935,21 @@ public class SatPlayground ...@@ -881,21 +935,21 @@ public class SatPlayground
nop( " return v;" ) nop( " return v;" )
), ),
elseseq( " } else { // loaded == INVALID || VALID ", elseseq( " } else { // loaded == INVALID || VALID ",
getv( " v = entry.getValue();", v4 ), getv( " v = entry.getValue();", v4 ),
branch( cond( v4, B, C ), branch( cond( v4, B, C ),
ifseq( " if ( v != null ) { ", ifseq( " if ( v != null ) { ",
nop( " return v;") nop( " return v;")
), ),
elseseq( " } else { // v == null ", elseseq( " } else { // v == null ",
remove( " map.remove( key, entry );" ), remove( " map.remove( key, entry );" ),
nop( " return get( key, loader, hints );" ) nop( " return get( key, loader, hints );" )
) )
) )
) )
) )
), ),
elseseq( "} else { // v != null ", elseseq( "} else { // v != null ",
nop( " return v; // strong ref (1)" ) nop( " return v; // strong ref (1)" )
) )
) )
); );
...@@ -904,48 +958,156 @@ public class SatPlayground ...@@ -904,48 +958,156 @@ public class SatPlayground
System.out.println(); System.out.println();
System.out.println(); System.out.println();
System.out.println( "CacheHints == BUDGETED" ); System.out.println( "CacheHints == BLOCKING" );
System.out.println( "======================" ); System.out.println( "======================" );
p = seq
(
init( "entry = computeIfAbsent()" ),
getv( "v = entry.getValue();", v1 ),
branch( cond( v1, B, C ),
ifseq( "if ( v != null ) {",
branch( cond( v1, C ),
ifseq( " if ( v.isValid() )",
nop( " return v;" )
),
elseseq( " } else {",
nop( " // continue below..." )
)
)
),
elseseq( "} // else {",
lock( "synchronized ( entry ) {" ),
branch(
cond( C, D, E, F ),
ifseq( " if ( loaded == VALID ) {",
getv( " v = entry.getValue();", v2 ),
branch( cond( v2, A, D, E, F ),
ifseq( " if ( v == null ) {",
remove( " map.remove( key, entry );" ),
nop( " return get( key, loader, hints );" )
),
elseseq( " } else {",
nop( " return v;" )
)
)
),
cond( A, B, D, E, F ),
elseseq( " } else { // loaded == NOTLOADED || INVALID",
unlock( "} // end synchronization" ),
nop( "lv = backingCache.get( key, loader );" ),
lock( "synchronized ( entry ) {" ),
getv( " v = entry.getValue();", v3 ),
branch(
cond( C, D, E, F ),
ifseq( " if ( loaded == VALID ) {",
branch( cond( v3, A, D, E, F ),
ifseq( " if ( v == null ) {",
remove( " map.remove( key, entry );" ),
nop( " return get( key, loader, hints );" )
),
elseseq( " } else {",
nop( " return v;" )
)
)
),
cond( A, B, D, E, F ),
elseseq( " } else { // loaded == NOTLOADED || INVALID",
branch( cond( A ),
ifseq( " if ( loaded == NOTLOADED ) { ",
setv( " entry.setValid( lv );", v4 ),
nop( " notifyAll();" ),
nop( " return lv;" )
),
elseseq( " } else {",
branch( cond( v3, A, D, E, F ),
ifseq( " if ( v == null ) {",
remove( " map.remove( key, entry );" ),
nop( " return get( key, loader, hints );" )
),
elseseq( " } else {",
setv( " entry.setValid( lv );", v5 ),
nop( " notifyAll();" ),
nop( " return lv;" )
)
)
)
)
)
)
)
)
)
)
);
p.recursivelyPrintPossibleStates();
System.out.println(); System.out.println();
System.out.println(); System.out.println();
System.out.println( "CacheHints == BLOCKING" ); System.out.println( "CacheHints == BUDGETED" );
System.out.println( "======================" ); System.out.println( "======================" );
p = seq p = seq
( (
init( "entry = computeIfAbsent();" ), init( "entry = computeIfAbsent()" ),
getv( "v = entry.getValue();", v1 ), getv( "v = entry.getValue();", v1 ),
branch( cond( v1, A, D, E, F ), branch( cond( v1, B, C ),
ifseq( "if ( v == null ) {", ifseq( "if ( v != null ) {",
lock( " synchronized ( entry ) {" ), branch( cond( v1, C ),
branch( cond( A ), ifseq( " if ( v.isValid() ) {",
ifseq( " if ( loaded == NOTLOADED ) {", nop( " return v;" )
nop( " v = loader.getInvalid();" ),
seti( " entry.setInvalid( v );", v2 ),
nop( " return v;" )
), ),
elseseq( " } else { // loaded == INVALID || VALID ", elseseq( " } else {",
getv( " v = entry.getValue();", v4 ), nop( " // continue below" )
branch( cond( v4, B, C ), )
ifseq( " if ( v != null ) { ", )
nop( " return v;") ),
elseseq( "} // else {",
lock( "synchronized ( entry ) {" ),
branch(
cond( C, D, E, F ),
ifseq( " if ( loaded == VALID )",
getv( " v = entry.getValue();", v2 ),
branch( cond( v2, A, D, E, F ),
ifseq( " if ( v == null ) {",
remove( " map.remove( key, entry );" ),
nop( " return get( key, loader, hints );" )
),
elseseq( " } else {",
nop( " return v;" )
)
)
),
cond( A, B, D, E, F ),
elseseq( " } else { // loaded == NOTLOADED || INVALID",
nop( " enqueue();" ),
unlock( " entry.wait( timeLeft ); // releases lock" ),
lock( " // lock reacquired" ),
branch( cond( B, C, D, E, F ),
ifseq( " if ( loaded == VALID || INVALID ) {",
getv( " v = entry.getValue();", v3 ),
branch( cond( v3, A, D, E, F ),
ifseq( " if ( v == null ) {",
remove( " map.remove( key, entry );" ),
nop( " return get( key, loader, hints );" )
),
elseseq( " } else {",
nop( " return v;" )
)
)
), ),
elseseq( " } else { // v == null ", elseseq( " } else { // loaded == NOTLOADED",
remove( " map.remove( key, entry );" ), getv( " v = loader.getInvalid();", v4 ),
nop( " return get( key, loader, hints );" ) seti( " entry.setInvalid( v );", v4 ),
nop( " return v;" )
) )
) )
) )
) )
),
elseseq( "} else { // v != null ",
nop( " return v; // strong ref (1)" )
) )
) )
); );
p.recursivelyPrintPossibleStates(); p.recursivelyPrintPossibleStates();
} }
} }
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment