lorin

\* Queue model where changes happen in each state
---- MODULE queue1 ----
EXTENDS Sequences

CONSTANT Val, N
VARIABLES op,arg,rval,d

none == CHOOSE v : v \notin Val

lorin

  org.springframework.web.util.NestedServletException: Handler dispatch failed; nested exception is java.lang.StackOverflowError
  	at org.springframework.web.servlet.DispatcherServlet.doDispatch(DispatcherServlet.java:1055) ~[spring-webmvc-5.2.3.RELEASE.jar:5.2.3.RELEASE]
  	at org.springframework.web.servlet.DispatcherServlet.doService(DispatcherServlet.java:943) ~[spring-webmvc-5.2.3.RELEASE.jar:5.2.3.RELEASE]
  	at org.springframework.web.servlet.FrameworkServlet.processRequest(FrameworkServlet.java:1006) [spring-webmvc-5.2.3.RELEASE.jar:5.2.3.RELEASE]
  	at org.springframework.web.servlet.FrameworkServlet.doGet(FrameworkServlet.java:898) [spring-webmvc-5.2.3.RELEASE.jar:5.2.3.RELEASE]
  	at javax.servlet.http.HttpServlet.service(HttpServlet.java:634) ~[tomcat-embed-core-9.0.30.jar:9.0.30]
  	at org.springframework.web.servlet.FrameworkServlet.service(FrameworkServlet.java:883) [spring-webmvc-5.2.3.RELEASE.jar:5.2.3.RELEASE]
  	at org.springframework.test.web.servlet.TestDispatcherServlet.service(TestDisp

lorin

##[group]Run ./gradlew build
./gradlew build
shell: /bin/bash -e {0}
env:
  GRADLE_OPTS: -Dorg.gradle.daemon=false -Xmx2g -Xms2g
  JAVA_HOME: /opt/hostedtoolcache/jdk/8.0.252/x64
  JAVA_HOME_8.0.252_x64: /opt/hostedtoolcache/jdk/8.0.252/x64
##[endgroup]
Downloading https://services.gradle.org/distributions/gradle-6.4-bin.zip
.........10%..........20%..........30%..........40%.........50%..........60%..........70%..........80%.........90%..........100%

lorin

2020-05-07 23:04:08
Full thread dump OpenJDK 64-Bit Server VM (25.251-b09 mixed mode):

"default connection adder" #5051 daemon prio=5 os_prio=0 tid=0x00007efd742bb000 nid=0x73f5 waiting on condition [0x00007efd72ae8000]
   java.lang.Thread.State: TIMED_WAITING (parking)
	at sun.misc.Unsafe.park(Native Method)
	- parking to wait for  <0x00000006d2ff9eb8> (a java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject)
	at java.util.concurrent.locks.LockSupport.parkNanos(LockSupport.java:215)
	at java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject.awaitNanos(AbstractQueuedSynchronizer.java:2083)
	at java.util.concurrent.LinkedBlockingQueue.poll(LinkedBlockingQueue.java:467)

lorin

java.lang.OutOfMemoryError: unable to create new native thread
	at java.lang.Thread.start0(Native Method)
	at java.lang.Thread.start(Thread.java:717)
	at java.util.concurrent.ThreadPoolExecutor.addWorker(ThreadPoolExecutor.java:957)
	at java.util.concurrent.ThreadPoolExecutor.execute(ThreadPoolExecutor.java:1367)
	at io.sentry.connection.AsyncConnection.send(AsyncConnection.java:96)
	at io.sentry.SentryClient.sendEvent(SentryClient.java:135)
	at io.sentry.SentryClient.sendEvent(SentryClient.java:152)
	at io.sentry.Sentry.capture(Sentry.java:215)
	at io.sentry.logback.SentryAppender.append(SentryAppender.java:106)

lorin

createBean:517, AbstractAutowireCapableBeanFactory (org.springframework.beans.factory.support) [3]
lambda$doGetBean$0:323, AbstractBeanFactory (org.springframework.beans.factory.support)
getObject:-1, 1709321711 (org.springframework.beans.factory.support.AbstractBeanFactory$$Lambda$233)
getSingleton:222, DefaultSingletonBeanRegistry (org.springframework.beans.factory.support)
doGetBean:321, AbstractBeanFactory (org.springframework.beans.factory.support)
getBean:202, AbstractBeanFactory (org.springframework.beans.factory.support)
getBeansWithAnnotation:666, DefaultListableBeanFactory (org.springframework.beans.factory.support)
getBeansWithAnnotation:1264, AbstractApplicationContext (org.springframework.context.support)
resolve:44, SpringPackageVersionResolver (com.netflix.spinnaker.kork.version)
resolve:57, ServiceVersion (com.netflix.spinnaker.kork.version)

lorin

2020-04-06 17:19:04
Full thread dump OpenJDK 64-Bit Server VM (25.241-b08 mixed mode):

"default connection adder" #1166 daemon prio=5 os_prio=0 tid=0x0000000000743000 nid=0x2bdf waiting on condition [0x00007efcb3a33000]
   java.lang.Thread.State: TIMED_WAITING (parking)
	at sun.misc.Unsafe.park(Native Method)
	- parking to wait for  <0x00000006d204d2d0> (a java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject)
	at java.util.concurrent.locks.LockSupport.parkNanos(LockSupport.java:215)
	at java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject.awaitNanos(AbstractQueuedSynchronizer.java:2083)
	at java.util.concurrent.LinkedBlockingQueue.poll(LinkedBlockingQueue.java:467)

lorin

Keybase proof

I hereby claim:

• I am lorin on github.
• I am lorin (https://keybase.io/lorin) on keybase.
• I have a public key ASBR2Fv6tYAWlp-BmSRLhBNCWqAE5ZE3dj25dwiEJFv_6go

To claim this, I am signing this object:

lorin

EXTENDS Naturals

CONSTANT N

(*
--algorithm Increment

variable count=0;

process Proc \in 1..N

lorin

------------------------------- MODULE Simple -------------------------------

\* From "Teaching Concurrency" by Leslie Lamport
\* https://www.microsoft.com/en-us/research/publication/teaching-concurrency/
\* See also: https://stackoverflow.com/a/46108331/742

EXTENDS Naturals, TLAPS

CONSTANTS N