aboutsummaryrefslogtreecommitdiffstats
path: root/os/kernel/src/chmemcore.c
blob: 0ff26bc76d78eb1a13aafeddccbb9b0ed81b78c2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
/*
    ChibiOS/RT - Copyright (C) 2006,2007,2008,2009,2010,
                 2011,2012,2013 Giovanni Di Sirio.

    This file is part of ChibiOS/RT.

    ChibiOS/RT is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 3 of the License, or
    (at your option) any later version.

    ChibiOS/RT is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.
*/

/**
 * @file    chmemcore.c
 * @brief   Core memory manager code.
 *
 * @addtogroup memcore
 * @details Core Memory Manager related APIs and services.
 *          <h2>Operation mode</h2>
 *          The core memory manager is a simplified allocator that only
 *          allows to allocate memory blocks without the possibility to
 *          free them.<br>
 *          This allocator is meant as a memory blocks provider for the
 *          other allocators such as:
 *          - C-Runtime allocator (through a compiler specific adapter module).
 *          - Heap allocator (see @ref heaps).
 *          - Memory pools allocator (see @ref pools).
 *          .
 *          By having a centralized memory provider the various allocators
 *          can coexist and share the main memory.<br>
 *          This allocator, alone, is also useful for very simple
 *          applications that just require a simple way to get memory
 *          blocks.
 * @pre     In order to use the core memory manager APIs the @p CH_USE_MEMCORE
 *          option must be enabled in @p chconf.h.
 * @{
 */

#include "ch.h"

#if CH_USE_MEMCORE || defined(__DOXYGEN__)

static uint8_t *nextmem;
static uint8_t *endmem;

/**
 * @brief   Low level memory manager initialization.
 *
 * @notapi
 */
void _core_init(void) {
#if CH_MEMCORE_SIZE == 0
  extern uint8_t __heap_base__[];
  extern uint8_t __heap_end__[];
  nextmem = (uint8_t *)MEM_ALIGN_NEXT(__heap_base__);
  endmem = (uint8_t *)MEM_ALIGN_PREV(__heap_end__);
#else
  static stkalign_t buffer[MEM_ALIGN_NEXT(CH_MEMCORE_SIZE)/MEM_ALIGN_SIZE];
  nextmem = (uint8_t *)&buffer[0];
  endmem = (uint8_t *)&buffer[MEM_ALIGN_NEXT(CH_MEMCORE_SIZE)/MEM_ALIGN_SIZE];
#endif
}

/**
 * @brief   Allocates a memory block.
 * @details The size of the returned block is aligned to the alignment
 *          type so it is not possible to allocate less
 *          than <code>MEM_ALIGN_SIZE</code>.
 *
 * @param[in] size      the size of the block to be allocated
 * @return              A pointer to the allocated memory block.
 * @retval NULL         allocation failed, core memory exhausted.
 *
 * @api
 */
void *chCoreAlloc(size_t size) {
  void *p;

  chSysLock();
  p = chCoreAllocI(size);
  chSysUnlock();
  return p;
}

/**
 * @brief   Allocates a memory block.
 * @details The size of the returned block is aligned to the alignment
 *          type so it is not possible to allocate less than
 *          <code>MEM_ALIGN_SIZE</code>.
 *
 * @param[in] size      the size of the block to be allocated.
 * @return              A pointer to the allocated memory block.
 * @retval NULL         allocation failed, core memory exhausted.
 *
 * @iclass
 */
void *chCoreAllocI(size_t size) {
  void *p;

  chDbgCheckClassI();

  size = MEM_ALIGN_NEXT(size);
  if ((size_t)(endmem - nextmem) < size)
    return NULL;
  p = nextmem;
  nextmem += size;
  return p;
}

/**
 * @brief   Core memory status.
 *
 * @return              The size, in bytes, of the free core memory.
 *
 * @api
 */
size_t chCoreStatus(void) {

  return (size_t)(endmem - nextmem);
}
#endif /* CH_USE_MEMCORE */

/** @} */
class="nb">true, bool turn_off_simp = false); lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); bool solve ( bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. // Memory managment: // virtual void garbageCollect(); // Generate a (possibly simplified) DIMACS file: // #if 0 void toDimacs (const char* file, const vec<Lit>& assumps); void toDimacs (const char* file); void toDimacs (const char* file, Lit p); void toDimacs (const char* file, Lit p, Lit q); void toDimacs (const char* file, Lit p, Lit q, Lit r); #endif // Mode of operation: // int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero). int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit. // -1 means no limit. int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit. double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac'). bool use_asymm; // Shrink clauses by asymmetric branching. bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :) bool use_elim; // Perform variable elimination. bool extend_model; // Flag to indicate whether the user needs to look at the full model. // Statistics: // int merges; int asymm_lits; int eliminated_vars; protected: // Helper structures: // struct ElimLt { const LMap<int>& n_occ; explicit ElimLt(const LMap<int>& no) : n_occ(no) {} // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating // 32-bit implementation instead then, but this will have to do for now. uint64_t cost (Var x) const { return (uint64_t)n_occ[mkLit(x)] * (uint64_t)n_occ[~mkLit(x)]; } bool operator()(Var x, Var y) const { return cost(x) < cost(y); } // TODO: investigate this order alternative more. // bool operator()(Var x, Var y) const { // int c_x = cost(x); // int c_y = cost(y); // return c_x < c_y || c_x == c_y && x < y; } }; struct ClauseDeleted { const ClauseAllocator& ca; explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {} bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } }; // Solver state: // int elimorder; bool use_simplification; Var max_simp_var; // Max variable at the point simplification was turned off. vec<uint32_t> elimclauses; VMap<char> touched; OccLists<Var, vec<CRef>, ClauseDeleted> occurs; LMap<int> n_occ; Heap<Var,ElimLt> elim_heap; Queue<CRef> subsumption_queue; VMap<char> frozen; vec<Var> frozen_vars; VMap<char> eliminated; int bwdsub_assigns; int n_touched; // Temporaries: // CRef bwdsub_tmpunit; // Main internal methods: // lbool solve_ (bool do_simp = true, bool turn_off_simp = false); bool asymm (Var v, CRef cr); bool asymmVar (Var v); void updateElimHeap (Var v); void gatherTouchedClauses (); bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause); bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size); bool backwardSubsumptionCheck (bool verbose = false); bool eliminateVar (Var v); void extendModel (); void removeClause (CRef cr); bool strengthenClause (CRef cr, Lit l); bool implied (const vec<Lit>& c); void relocAll (ClauseAllocator& to); }; //================================================================================================= // Implementation of inline methods: inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; } inline void SimpSolver::updateElimHeap(Var v) { assert(use_simplification); // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef) if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)) elim_heap.update(v); } inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); } inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); } inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); } inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); } inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, Lit s){ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); add_tmp.push(s); return addClause_(add_tmp); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } inline void SimpSolver::freezeVar(Var v){ if (!frozen[v]){ frozen[v] = 1; frozen_vars.push(v); } } inline void SimpSolver::thaw(){ for (int i = 0; i < frozen_vars.size(); i++){ Var v = frozen_vars[i]; frozen[v] = 0; if (use_simplification) updateElimHeap(v); } frozen_vars.clear(); } inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; } inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; } inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; } inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; } inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; } inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } //================================================================================================= } #endif