To protect your data, the CISO officer has suggested users to enable 2FA as soon as possible.
Currently 2.7% of users enabled 2FA.

  1. 16 Nov, 2017 1 commit
  2. 28 Sep, 2017 1 commit
    • Adam Nelson's avatar
      Partial work on optimizationsTheory · a52438d8
      Adam Nelson authored
      uvmOptimizationsTheory proves the validity of optimizations on Mu
      bytecode. Incomplete proofs are stubbed out with "cheat" or commented
      out.
      a52438d8
  3. 02 Sep, 2017 2 commits
  4. 31 Aug, 2017 1 commit
  5. 30 Aug, 2017 2 commits
  6. 25 Aug, 2017 1 commit
    • Adam Nelson's avatar
      Rearrange helper files, add syntax sugar · 296c77dc
      Adam Nelson authored
      - Split up DefineUtils into separate files following the HOL convention
        (e.g., fooScript + fooLib)
      - sumMonadTheory merged into monadsTheory, which now contains list and
        option monads as well
      - List and option monads used to clean up code throughout the project
      - Extra unicode symbols/operators in syntaxSugarTheory
      296c77dc
  7. 24 Aug, 2017 1 commit
    • Adam Nelson's avatar
      Tests pass again with RISC-V code! · 87ce7ba5
      Adam Nelson authored
      - Parser updated to work with code changes
      - Lots of bug fixes to get tests to pass (previous commit didn't even
        execute basic instructions properly)
      - Improved pretty printing and EVAL
      87ce7ba5
  8. 20 Aug, 2017 1 commit
    • Adam Nelson's avatar
      Atomic memory cells and operations for WMM/RISC-V · 59737ac5
      Adam Nelson authored
      - Memory and registers are split up into typed atomic cells
      - Value type now contains only scalar values
      - Instructions are compiled down to WMM "operations", allowing stores
        and loads of composite values to be split up into atomic parts
      - Scheduler now executes one operation at a time, rather than one block
        at a time
      - New scheduler steps for WMM
      - Commands (formerly Thread Actions) such as allocation now executed at
        the global scheduler level. Action IDs no longer needed.
      - Threads and stacks changed completely; registers now stored in stack
        frames
      - Monads pretty-print properly again!
      - Patricia trees replaced with sptrees
      
      Lots of code is still commented out, and tests still don't work, but
      the main formalization code compiles.
      59737ac5
  9. 20 Jul, 2017 1 commit
  10. 25 Jun, 2017 1 commit
    • Adam Nelson's avatar
      More progress on RISC-V, change pop-frame process · b1d3c66c
      Adam Nelson authored
      - Free was changed from a store message to a thread_action message
      - Stack frames are now freed properly when returning from a function
      - Heap/stack addresses are tracked separately again
      - New stores are added to invalidation buffers, per the spec
      - Thread actions are executed now
      - Tests still don't work yet
      b1d3c66c
  11. 22 Jun, 2017 1 commit
  12. 06 Jun, 2017 1 commit
  13. 05 May, 2017 1 commit
    • Adam Nelson's avatar
      Prove local seq consistency for seq_cst_schedule · fb68640a
      Adam Nelson authored
      It's finally done! The first memory consistency proof in the formalization:
      a sequentially consistent schedule (one that always commits memory messages
      from the front of a thread's outbox queue) will always produce locally
      sequentially consistent semantics.
      
      Changes made in the process of this proof include:
      
      - Removed thread IDs and stack IDs from the thread and stack records;
        keeping up with invariants for them was pointless bookkeeping
      
      - Defined custom tactics multi_case_tac and rw_assums, which greatly
        reduced the size and complexity of some proofs
      
      - Added several new invariants to state_ok, including memory consistency
        invariants (committed messages are all distinct, no message can be in
        both the commit list and a thread's outbox, etc.)
      fb68640a
  14. 05 Apr, 2017 1 commit
  15. 03 Apr, 2017 1 commit
  16. 02 Apr, 2017 1 commit
  17. 01 Apr, 2017 1 commit
  18. 31 Mar, 2017 1 commit
  19. 30 Mar, 2017 1 commit
  20. 28 Mar, 2017 1 commit
  21. 26 Mar, 2017 1 commit
  22. 15 Mar, 2017 1 commit
  23. 11 Mar, 2017 1 commit
  24. 07 Mar, 2017 1 commit
    • Adam Nelson's avatar
      Parser improvements, comminst support · dea983cd
      Adam Nelson authored
      Removed a special case in the parser for FuncRefV constants, which
      required every SSA variable to have a known type. This required
      BundleParser to be rearranged to parse everything else before function
      bodies, making functions available to functions defined above them
      (something the spec requires, so that's progress!)
      
      Also added support for COMMINST in the parser.
      dea983cd
  25. 02 Mar, 2017 1 commit
    • Adam Nelson's avatar
      Split up uvmThreadSemantics, add 'ok' predicates · ff7ff016
      Adam Nelson authored
      uvmThreadSemantics was becoming a huge file that took several minutes
      to compile, so it's been split into uvmThreadsStacks and
      uvmInstructionSemantics.
      
      In uvmThreadsStacks, new 'thread_ok' and 'stack_ok' predicates define
      basic consistency requirements for thread and stack data structures.
      All functions in this file have also been proven to produce valid
      thread/stack structures when given valid input. This is a prerequisite
      for proving execution state homomorphisms.
      
      'thread_state' has been renamed to 'thread', and 'state_follows' has
      been renamed to 'thread_follows'.
      ff7ff016
  26. 24 Feb, 2017 1 commit
    • Adam Nelson's avatar
      Clean up exec_terminst, remove $-variables · d4b31059
      Adam Nelson authored
      The current version of the Mu specification does not use $-variables to
      pass return values from terminsts to the normal destination of an EXC
      clause, instead allowing terminsts to have normal SSA return values
      that may be referenced in the EXC clause. This commit updates the
      formalism to match.
      
      Several other refactorings are included, such as making exec_terminst
      only return modified stacks, using a simpler representation of common
      instructions, and defining prefix/infix operators for SSA variables and
      registers in HOL.
      d4b31059
  27. 22 Feb, 2017 1 commit
  28. 16 Feb, 2017 1 commit
  29. 07 Feb, 2017 1 commit
    • Adam Nelson's avatar
      Support for spawning new threads · 4732dc3b
      Adam Nelson authored
      The NEWTHREAD instruction isn't parsed yet, but its associated memory message is
      now supported, and the scheduler has been modified to support multiple threads.
      
      thread_states are now generated on-demand when they are first executed, provided
      there is an associated DoNewThread memory action and its stack ID can be
      resolved. This required the 'tid' field of 'Message' to be changed to a
      'thread_id option', as there must be an initial DoNewThread action that is not
      generated by any thread ID.
      
      The THROW instruction and EXC resume_values have also been updated to have only
      one argument, to match the spec.
      4732dc3b
  30. 01 Feb, 2017 1 commit
    • Alexander Soen's avatar
      Change list translation method · 2d935438
      Alexander Soen authored
      Translation method now uses an intermediary type datastructure.
      It is similar to the previous method which was done in two stages.
      
      To do:
        - Clean up code base
        - Add abstractions
        - Fix the testing script
      2d935438
  31. 27 Jan, 2017 2 commits
    • Alexander Soen's avatar
      Add translate_interm tests · 99edb424
      Alexander Soen authored
      99edb424
    • Alexander Soen's avatar
      Change translation method · ed21b02d
      Alexander Soen authored
      The translation method has been changed into two phases. The first is to
      determine the final type of what the translated term would be. The
      second, is with this type information, to create the final translated
      term.
      
      To do:
        -- Implement abstractions for translation
      ed21b02d
  32. 24 Jan, 2017 1 commit
  33. 23 Jan, 2017 2 commits
  34. 19 Jan, 2017 2 commits
  35. 18 Jan, 2017 1 commit
    • Alexander Soen's avatar
      Translation of sets of sets now possible · 2e0a1c69
      Alexander Soen authored
      Currently the expected translation function works for constants. This
      needs to be extended for other term types.
      
      The robustness of the type inference can also be improved on.
      Currently the new type is generated by appending new elements to a list
      which has an implicit ordering.
      2e0a1c69