improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
authorwenzelm
Mon Apr 28 16:17:07 2014 +0200 (2014-04-28)
changeset 5677559f70b89e5fd
parent 56774 2d39c313f39e
child 56776 309e1a61ee7c
improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
src/Pure/PIDE/session.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/syslog_dockable.scala
     1.1 --- a/src/Pure/PIDE/session.scala	Mon Apr 28 15:29:09 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Mon Apr 28 16:17:07 2014 +0200
     1.3 @@ -75,6 +75,27 @@
     1.4    //}}}
     1.5  
     1.6  
     1.7 +  /* syslog */
     1.8 +
     1.9 +  private[Session] class Syslog(limit: Int)
    1.10 +  {
    1.11 +    private var queue = Queue.empty[XML.Elem]
    1.12 +    private var length = 0
    1.13 +
    1.14 +    def += (msg: XML.Elem): Unit = synchronized {
    1.15 +      queue = queue.enqueue(msg)
    1.16 +      length += 1
    1.17 +      if (length > limit) queue = queue.dequeue._2
    1.18 +    }
    1.19 +
    1.20 +    def content: String = synchronized {
    1.21 +      cat_lines(queue.iterator.map(XML.content)) +
    1.22 +      (if (length > limit) "\n(A total of " + length + " messages...)" else "")
    1.23 +    }
    1.24 +  }
    1.25 +
    1.26 +
    1.27 +
    1.28    /* protocol handlers */
    1.29  
    1.30    abstract class Protocol_Handler
    1.31 @@ -207,8 +228,8 @@
    1.32  
    1.33    /* global state */
    1.34  
    1.35 -  private val syslog = Synchronized(Queue.empty[XML.Elem])
    1.36 -  def current_syslog(): String = cat_lines(syslog.value.iterator.map(XML.content))
    1.37 +  private val syslog = new Session.Syslog(syslog_limit)
    1.38 +  def syslog_content(): String = syslog.content
    1.39  
    1.40    @volatile private var _phase: Session.Phase = Session.Inactive
    1.41    private def phase_=(new_phase: Session.Phase)
    1.42 @@ -476,16 +497,15 @@
    1.43          //{{{
    1.44          arg match {
    1.45            case output: Prover.Output =>
    1.46 -            if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
    1.47 +            if (output.is_stdout || output.is_stderr)
    1.48 +              raw_output_messages.post(output)
    1.49              else handle_output(output)
    1.50 +
    1.51              if (output.is_syslog) {
    1.52 -              syslog.change(queue =>
    1.53 -                {
    1.54 -                  val queue1 = queue.enqueue(output.message)
    1.55 -                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
    1.56 -                })
    1.57 +              syslog += output.message
    1.58                syslog_messages.post(output)
    1.59              }
    1.60 +
    1.61              all_messages.post(output)
    1.62  
    1.63            case input: Prover.Input =>
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 28 15:29:09 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 28 16:17:07 2014 +0200
     2.3 @@ -249,7 +249,7 @@
     2.4        case Session.Inactive | Session.Failed =>
     2.5          Swing_Thread.later {
     2.6            GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
     2.7 -              "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
     2.8 +            "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
     2.9          }
    2.10  
    2.11        case Session.Ready =>
     3.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Mon Apr 28 15:29:09 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Mon Apr 28 16:17:07 2014 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  
     3.5  import isabelle._
     3.6  
     3.7 -import scala.swing.TextArea
     3.8 +import scala.swing.{TextArea, ScrollPane}
     3.9  
    3.10  import org.gjt.sp.jedit.View
    3.11  
    3.12 @@ -20,29 +20,24 @@
    3.13  
    3.14    private val syslog = new TextArea()
    3.15  
    3.16 -  private def update_syslog()
    3.17 +  private def syslog_delay = Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
    3.18    {
    3.19 -    Swing_Thread.require {}
    3.20 -
    3.21 -    val text = PIDE.session.current_syslog()
    3.22 +    val text = PIDE.session.syslog_content()
    3.23      if (text != syslog.text) syslog.text = text
    3.24    }
    3.25  
    3.26 -  set_content(syslog)
    3.27 +  set_content(new ScrollPane(syslog))
    3.28  
    3.29  
    3.30    /* main */
    3.31  
    3.32    private val main =
    3.33 -    Session.Consumer[Prover.Output](getClass.getName) {
    3.34 -      case output =>
    3.35 -        if (output.is_syslog) Swing_Thread.later { update_syslog() }
    3.36 -    }
    3.37 +    Session.Consumer[Prover.Output](getClass.getName) { case _ => syslog_delay.invoke() }
    3.38  
    3.39    override def init()
    3.40    {
    3.41      PIDE.session.syslog_messages += main
    3.42 -    update_syslog()
    3.43 +    syslog_delay.invoke()
    3.44    }
    3.45  
    3.46    override def exit()